Metamath Proof Explorer


Theorem intexab

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

Ref Expression
Assertion intexab
|- ( E. x ph <-> |^| { x | ph } e. _V )

Proof

Step Hyp Ref Expression
1 abn0
 |-  ( { x | ph } =/= (/) <-> E. x ph )
2 intex
 |-  ( { x | ph } =/= (/) <-> |^| { x | ph } e. _V )
3 1 2 bitr3i
 |-  ( E. x ph <-> |^| { x | ph } e. _V )