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 ⊢ A ∈ V → A ∈ ⋂ B ↔ ∀ x ∈ B A ∈ x
Proof
Step
Hyp
Ref
Expression
1
eleq1 ⊢ y = A → y ∈ x ↔ A ∈ x
2
1
ralbidv ⊢ y = A → ∀ x ∈ B y ∈ x ↔ ∀ x ∈ B A ∈ x
3
dfint2 ⊢ ⋂ B = y | ∀ x ∈ B y ∈ x
4
2 3
elab2g ⊢ A ∈ V → A ∈ ⋂ B ↔ ∀ x ∈ B A ∈ x