This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem elint2

Description: Membership in class intersection. (Contributed by NM, 14-Oct-1999)

Ref Expression
Hypothesis elint2.1 ⊢ A ∈ V
Assertion elint2 ⊢ A ∈ ⋂ B ↔ ∀ x ∈ B A ∈ x

Proof

Step Hyp Ref Expression
1 elint2.1 ⊢ A ∈ V
2 1 elint ⊢ A ∈ ⋂ B ↔ ∀ x x ∈ B → A ∈ x
3 df-ral ⊢ ∀ x ∈ B A ∈ x ↔ ∀ x x ∈ B → A ∈ x
4 2 3 bitr4i ⊢ A ∈ ⋂ B ↔ ∀ x ∈ B A ∈ x