Metamath Proof Explorer


Theorem intexab

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

Ref Expression
Assertion intexab ( ∃ 𝑥 𝜑 { 𝑥𝜑 } ∈ V )

Proof

Step Hyp Ref Expression
1 abn0 ( { 𝑥𝜑 } ≠ ∅ ↔ ∃ 𝑥 𝜑 )
2 intex ( { 𝑥𝜑 } ≠ ∅ ↔ { 𝑥𝜑 } ∈ V )
3 1 2 bitr3i ( ∃ 𝑥 𝜑 { 𝑥𝜑 } ∈ V )