This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ZF (ZERMELO-FRAENKEL) SET THEORY ZF Set Theory - start with the Axiom of Extensionality The intersection of a class 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 ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ ∩ 𝐵 ↔ ∀ 𝑥 ∈ 𝐵 𝐴 ∈ 𝑥 ) )