ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  0ex Structured version   GIF version

Theorem 0ex 3854
Description: The Null Set Axiom of ZF set theory: the empty set exists. Corollary 5.16 of [TakeutiZaring] p. 20. For the unabbreviated version, see ax-nul 3853. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
Assertion
Ref Expression
0ex V

Proof of Theorem 0ex
Dummy variables x y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ax-nul 3853 . . 3 xy ¬ y x
2 eq0 3212 . . . 4 (x = ∅ ↔ y ¬ y x)
32exbii 1474 . . 3 (x x = ∅ ↔ xy ¬ y x)
41, 3mpbir 134 . 2 x x = ∅
54issetri 2538 1 V
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wal 1224   = wceq 1226  wex 1358   wcel 1370  Vcvv 2531  c0 3197
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 532  ax-in2 533  ax-io 617  ax-5 1312  ax-7 1313  ax-gen 1314  ax-ie1 1359  ax-ie2 1360  ax-8 1372  ax-10 1373  ax-11 1374  ax-i12 1375  ax-bnd 1376  ax-4 1377  ax-17 1396  ax-i9 1400  ax-ial 1405  ax-i5r 1406  ax-ext 2000  ax-nul 3853
This theorem depends on definitions:  df-bi 110  df-tru 1229  df-nf 1326  df-sb 1624  df-clab 2005  df-cleq 2011  df-clel 2014  df-nfc 2145  df-v 2533  df-dif 2893  df-nul 3198
This theorem is referenced by:  0elpw  3887  0nep0  3888  iin0r  3892  intv  3893  snexprc  3908  p0ex  3909  0elon  4074  onm  4083  ordtriexmidlem2  4189  ordtriexmid  4190  ordtri2orexmid  4191  onsucsssucexmid  4192  onsucelsucexmidlem1  4193  onsucelsucexmid  4195  regexmidlem1  4198  ordsoexmid  4220  ordpwsucexmid  4226  peano1  4240  finds  4246  finds2  4247  0elnn  4263  opthprc  4314  nfunv  4855  fun0  4879  acexmidlema  5423  acexmidlemb  5424  acexmidlemab  5426  ovprc  5459  1st0  5690  2nd0  5691  brtpos0  5785  reldmtpos  5786  rdgi0g  5882  rdg0  5891  frec0g  5898  1n0  5927  el1o  5931  fnom  5941  omexg  5942  om0  5949  nnsucsssuc  5982  bj-d0clsepcl  7287  bj-indint  7293  bj-bdfindis  7308  bj-inf2vnlem1  7327
  Copyright terms: Public domain W3C validator