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

Metamath Proof Explorer

Theorem intexab

Description: The intersection of a nonempty class abstraction exists. (Contributed by NM, 21-Oct-2003)

Ref Expression
Assertion intexab ⊢ ∃ x φ ↔ ⋂ x | φ ∈ V

Proof

Step Hyp Ref Expression
1 abn0 ⊢ x | φ ≠ ∅ ↔ ∃ x φ
2 intex ⊢ x | φ ≠ ∅ ↔ ⋂ x | φ ∈ V
3 1 2 bitr3i ⊢ ∃ x φ ↔ ⋂ x | φ ∈ V