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

Metamath Proof Explorer

Theorem elintabg

Description: Two ways of saying a set is an element of the intersection of a class. (Contributed by NM, 30-Aug-1993) Put in closed form. (Revised by RP, 13-Aug-2020)

Ref Expression
Assertion elintabg ⊢ A ∈ V → A ∈ ⋂ x | φ ↔ ∀ x φ → A ∈ x

Proof

Step Hyp Ref Expression
1 elintg ⊢ A ∈ V → A ∈ ⋂ x | φ ↔ ∀ y ∈ x | φ A ∈ y
2 eleq2w ⊢ y = x → A ∈ y ↔ A ∈ x
3 2 ralab2 ⊢ ∀ y ∈ x | φ A ∈ y ↔ ∀ x φ → A ∈ x
4 1 3 bitrdi ⊢ A ∈ V → A ∈ ⋂ x | φ ↔ ∀ x φ → A ∈ x