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		df-int	⊢ ∩ 𝐵 = { 𝑦 ∣ ∀ 𝑥 ( 𝑥 ∈ 𝐵 → 𝑦 ∈ 𝑥 ) }
6	4 5	elab2g	⊢ ( 𝐴 ∈ V → ( 𝐴 ∈ ∩ 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐵 → 𝐴 ∈ 𝑥 ) ) )
7	1 6	ax-mp	⊢ ( 𝐴 ∈ ∩ 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐵 → 𝐴 ∈ 𝑥 ) )