Theorem elintg

Description: Membership in class intersection, with the sethood requirement expressed as an antecedent. (Contributed by NM, 20-Nov-2003) (Proof shortened by JJ, 26-Jul-2021)

	Ref	Expression
Assertion	elintg	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ ∩ 𝐵 ↔ ∀ 𝑥 ∈ 𝐵 𝐴 ∈ 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		eleq1	⊢ ( 𝑦 = 𝐴 → ( 𝑦 ∈ 𝑥 ↔ 𝐴 ∈ 𝑥 ) )
2	1	ralbidv	⊢ ( 𝑦 = 𝐴 → ( ∀ 𝑥 ∈ 𝐵 𝑦 ∈ 𝑥 ↔ ∀ 𝑥 ∈ 𝐵 𝐴 ∈ 𝑥 ) )
3		dfint2	⊢ ∩ 𝐵 = { 𝑦 ∣ ∀ 𝑥 ∈ 𝐵 𝑦 ∈ 𝑥 }
4	2 3	elab2g	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ ∩ 𝐵 ↔ ∀ 𝑥 ∈ 𝐵 𝐴 ∈ 𝑥 ) )