Theorem elinti

Description: Membership in class intersection. (Contributed by NM, 14-Oct-1999) (Proof shortened by Andrew Salmon, 9-Jul-2011)

	Ref	Expression
Assertion	elinti	⊢ ( 𝐴 ∈ ∩ 𝐵 → ( 𝐶 ∈ 𝐵 → 𝐴 ∈ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		elintg	⊢ ( 𝐴 ∈ ∩ 𝐵 → ( 𝐴 ∈ ∩ 𝐵 ↔ ∀ 𝑥 ∈ 𝐵 𝐴 ∈ 𝑥 ) )
2		eleq2	⊢ ( 𝑥 = 𝐶 → ( 𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝐶 ) )
3	2	rspccv	⊢ ( ∀ 𝑥 ∈ 𝐵 𝐴 ∈ 𝑥 → ( 𝐶 ∈ 𝐵 → 𝐴 ∈ 𝐶 ) )
4	1 3	biimtrdi	⊢ ( 𝐴 ∈ ∩ 𝐵 → ( 𝐴 ∈ ∩ 𝐵 → ( 𝐶 ∈ 𝐵 → 𝐴 ∈ 𝐶 ) ) )
5	4	pm2.43i	⊢ ( 𝐴 ∈ ∩ 𝐵 → ( 𝐶 ∈ 𝐵 → 𝐴 ∈ 𝐶 ) )