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 )