This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem n0el

Description: Negated membership of the empty set in another class. (Contributed by Rodolfo Medina, 25-Sep-2010)

Ref Expression
Assertion n0el 
|- ( -. (/) e. A <-> A. x e. A E. u u e. x )

Proof

Step Hyp Ref Expression
1 df-ral 
 |-  ( A. x e. A -. A. u -. u e. x <-> A. x ( x e. A -> -. A. u -. u e. x ) )
2 df-ex 
 |-  ( E. u u e. x <-> -. A. u -. u e. x )
3 2 ralbii 
 |-  ( A. x e. A E. u u e. x <-> A. x e. A -. A. u -. u e. x )
4 alnex 
 |-  ( A. x -. ( x e. A /\ A. u -. u e. x ) <-> -. E. x ( x e. A /\ A. u -. u e. x ) )
5 imnang 
 |-  ( A. x ( x e. A -> -. A. u -. u e. x ) <-> A. x -. ( x e. A /\ A. u -. u e. x ) )
6 0el 
 |-  ( (/) e. A <-> E. x e. A A. u -. u e. x )
7 df-rex 
 |-  ( E. x e. A A. u -. u e. x <-> E. x ( x e. A /\ A. u -. u e. x ) )
8 6 7 bitri 
 |-  ( (/) e. A <-> E. x ( x e. A /\ A. u -. u e. x ) )
9 8 notbii 
 |-  ( -. (/) e. A <-> -. E. x ( x e. A /\ A. u -. u e. x ) )
10 4 5 9 3bitr4ri 
 |-  ( -. (/) e. A <-> A. x ( x e. A -> -. A. u -. u e. x ) )
11 1 3 10 3bitr4ri 
 |-  ( -. (/) e. A <-> A. x e. A E. u u e. x )