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		elequ1	⊢ ( 𝑧 = 𝑦 → ( 𝑧 ∈ 𝑥 ↔ 𝑦 ∈ 𝑥 ) )
2	1	ralbidv	⊢ ( 𝑧 = 𝑦 → ( ∀ 𝑥 ∈ 𝐵 𝑧 ∈ 𝑥 ↔ ∀ 𝑥 ∈ 𝐵 𝑦 ∈ 𝑥 ) )
3		eleq1	⊢ ( 𝑦 = 𝐴 → ( 𝑦 ∈ 𝑥 ↔ 𝐴 ∈ 𝑥 ) )
4	3	ralbidv	⊢ ( 𝑦 = 𝐴 → ( ∀ 𝑥 ∈ 𝐵 𝑦 ∈ 𝑥 ↔ ∀ 𝑥 ∈ 𝐵 𝐴 ∈ 𝑥 ) )
5		dfint2	⊢ ∩ 𝐵 = { 𝑧 ∣ ∀ 𝑥 ∈ 𝐵 𝑧 ∈ 𝑥 }
6	2 4 5	elab2gw	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ ∩ 𝐵 ↔ ∀ 𝑥 ∈ 𝐵 𝐴 ∈ 𝑥 ) )