Metamath Proof Explorer

Theorem rabn0

Description: Nonempty restricted class abstraction. (Contributed by NM, 29-Aug-1999) (Revised by BJ, 16-Jul-2021)

Ref Expression
Assertion rabn0 
|- ( { x e. A | ph } =/= (/) <-> E. x e. A ph )

Proof

Step Hyp Ref Expression
1 rabeq0 
 |-  ( { x e. A | ph } = (/) <-> A. x e. A -. ph )
2 1 necon3abii 
 |-  ( { x e. A | ph } =/= (/) <-> -. A. x e. A -. ph )
3 dfrex2 
 |-  ( E. x e. A ph <-> -. A. x e. A -. ph )
4 2 3 bitr4i 
 |-  ( { x e. A | ph } =/= (/) <-> E. x e. A ph )