HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem zfnuleu 2697
Description: Show the uniqueness of the empty set (using the Axiom of Extensionality via bm1.1 1455 to strengthen axnul 2699).
Hypothesis
Ref Expression
zfnuleu.1 |- E.xA.y -. y e. x
Assertion
Ref Expression
zfnuleu |- E!xA.y -. y e. x
Distinct variable group:   x,y
Proof of Theorem zfnuleu
StepHypRef Expression
1 zfnuleu.1 . . . 4 |- E.xA.y -. y e. x
2 equid 1122 . . . . . . 7 |- y = y
32nbn3 721 . . . . . 6 |- (-. y e. x <-> (y e. x <-> -. y = y))
43albii 996 . . . . 5 |- (A.y -. y e. x <-> A.y(y e. x <-> -. y = y))
54exbii 1047 . . . 4 |- (E.xA.y -. y e. x <-> E.xA.y(y e. x <-> -. y = y))
61, 5mpbi 189 . . 3 |- E.xA.y(y e. x <-> -. y = y)
7 ax-17 968 . . . 4 |- (-. y = y -> A.x -. y = y)
87bm1.1 1455 . . 3 |- (E.xA.y(y e. x <-> -. y = y) -> E!xA.y(y e. x <-> -. y = y))
96, 8ax-mp 7 . 2 |- E!xA.y(y e. x <-> -. y = y)
104eubii 1380 . 2 |- (E!xA.y -. y e. x <-> E!xA.y(y e. x <-> -. y = y))
119, 10mpbir 190 1 |- E!xA.y -. y e. x
Colors of variables: wff set class
Syntax hints:  -. wn 2   <-> wb 146  A.wal 951   = wceq 953   e. wcel 955  E.wex 977  E!weu 1373
This theorem is referenced by:  0ex 2701  snex 2740
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-11 964  ax-12 965  ax-14 967  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452
This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 978  df-sb 1168  df-eu 1375
Copyright terms: Public domain