Theorem elint

Description: Membership in class intersection. (Contributed by NM, 21-May-1994)

	Ref	Expression
Hypothesis	elint.1	⊢ 𝐴 ∈ V
Assertion	elint	⊢ ( 𝐴 ∈ ∩ 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐵 → 𝐴 ∈ 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		elint.1	⊢ 𝐴 ∈ V
2		eleq1	⊢ ( 𝑧 = 𝑦 → ( 𝑧 ∈ 𝑥 ↔ 𝑦 ∈ 𝑥 ) )
3	2	imbi2d	⊢ ( 𝑧 = 𝑦 → ( ( 𝑥 ∈ 𝐵 → 𝑧 ∈ 𝑥 ) ↔ ( 𝑥 ∈ 𝐵 → 𝑦 ∈ 𝑥 ) ) )
4	3	albidv	⊢ ( 𝑧 = 𝑦 → ( ∀ 𝑥 ( 𝑥 ∈ 𝐵 → 𝑧 ∈ 𝑥 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐵 → 𝑦 ∈ 𝑥 ) ) )
5		eleq1	⊢ ( 𝑦 = 𝐴 → ( 𝑦 ∈ 𝑥 ↔ 𝐴 ∈ 𝑥 ) )
6	5	imbi2d	⊢ ( 𝑦 = 𝐴 → ( ( 𝑥 ∈ 𝐵 → 𝑦 ∈ 𝑥 ) ↔ ( 𝑥 ∈ 𝐵 → 𝐴 ∈ 𝑥 ) ) )
7	6	albidv	⊢ ( 𝑦 = 𝐴 → ( ∀ 𝑥 ( 𝑥 ∈ 𝐵 → 𝑦 ∈ 𝑥 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐵 → 𝐴 ∈ 𝑥 ) ) )
8		df-int	⊢ ∩ 𝐵 = { 𝑧 ∣ ∀ 𝑥 ( 𝑥 ∈ 𝐵 → 𝑧 ∈ 𝑥 ) }
9	4 7 8	elab2gw	⊢ ( 𝐴 ∈ V → ( 𝐴 ∈ ∩ 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐵 → 𝐴 ∈ 𝑥 ) ) )
10	1 9	ax-mp	⊢ ( 𝐴 ∈ ∩ 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐵 → 𝐴 ∈ 𝑥 ) )