Metamath Proof Explorer

Theorem abn0

Description: Nonempty class abstraction. See also ab0 . (Contributed by NM, 26-Dec-1996) (Proof shortened by Mario Carneiro, 11-Nov-2016)

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

Proof

Step Hyp Ref Expression
1 nfab1 
 |-  F/_ x { x | ph }
2 1 n0f 
 |-  ( { x | ph } =/= (/) <-> E. x x e. { x | ph } )
3 abid 
 |-  ( x e. { x | ph } <-> ph )
4 3 exbii 
 |-  ( E. x x e. { x | ph } <-> E. x ph )
5 2 4 bitri 
 |-  ( { x | ph } =/= (/) <-> E. x ph )