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

Theorem 0ex 4061
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 4060. (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 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ax-nul 4060 . . 3 𝑥𝑦 ¬ 𝑦𝑥
2 eq0 3384 . . . 4 (𝑥 = ∅ ↔ ∀𝑦 ¬ 𝑦𝑥)
32exbii 1585 . . 3 (∃𝑥 𝑥 = ∅ ↔ ∃𝑥𝑦 ¬ 𝑦𝑥)
41, 3mpbir 145 . 2 𝑥 𝑥 = ∅
54issetri 2698 1 ∅ ∈ V
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wal 1330   = wceq 1332  wex 1469  wcel 1481  Vcvv 2689  c0 3366
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-nul 4060
This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-v 2691  df-dif 3076  df-nul 3367
This theorem is referenced by:  0elpw  4094  0nep0  4095  iin0r  4099  intv  4100  snexprc  4116  p0ex  4118  undifexmid  4123  exmidexmid  4126  exmid01  4127  exmidsssn  4131  exmidel  4134  exmidundif  4135  exmidundifim  4136  0elon  4320  onm  4329  ordtriexmidlem2  4442  ordtriexmid  4443  ordtri2orexmid  4444  ontr2exmid  4446  onsucsssucexmid  4448  onsucelsucexmidlem1  4449  onsucelsucexmid  4451  regexmidlem1  4454  reg2exmidlema  4455  ordsoexmid  4483  0elsucexmid  4486  ordpwsucexmid  4491  ordtri2or2exmid  4492  dcextest  4501  peano1  4514  finds  4520  finds2  4521  0elnn  4538  opthprc  4596  nfunv  5162  fun0  5187  acexmidlema  5771  acexmidlemb  5772  acexmidlemab  5774  ovprc  5812  1st0  6048  2nd0  6049  brtpos0  6155  reldmtpos  6156  tfr0dm  6225  rdg0  6290  frec0g  6300  1n0  6335  el1o  6340  0lt2o  6344  fnom  6352  omexg  6353  om0  6360  nnsucsssuc  6394  mapdm0  6563  map0e  6586  0elixp  6629  en0  6695  ensn1  6696  en1  6699  2dom  6705  map1  6712  xp1en  6723  endisj  6724  dom0  6738  php5dom  6763  ssfilem  6775  ssfiexmid  6776  domfiexmid  6778  diffitest  6787  ac6sfi  6798  exmidpw  6808  unfiexmid  6812  fi0  6869  djuexb  6935  djulclr  6940  djulcl  6942  djulclb  6946  djulf1or  6947  djulf1o  6949  inl11  6956  djuss  6961  1stinl  6965  2ndinl  6966  0ct  6998  finomni  7018  exmidomni  7020  exmidonfinlem  7064  exmidfodomrlemr  7073  exmidfodomrlemrALT  7074  exmidaclem  7079  dju0en  7085  djucomen  7087  djuassen  7088  xpdjuen  7089  indpi  7172  frecfzennn  10228  fihashen1  10575  hashunlem  10580  zfz1iso  10614  ennnfonelemj0  11943  ennnfonelem0  11947  ennnfonelemhom  11957  strsl0  12039  topgele  12228  en1top  12278  sn0topon  12289  sn0cld  12338  rest0  12380  restsn  12381  0met  12585  djulclALT  13172  bj-d0clsepcl  13287  bj-indint  13293  bj-bdfindis  13309  bj-inf2vnlem1  13332  pw1dom2  13354  pwle2  13359  exmid1stab  13361  pw1nct  13364  0nninf  13365  nninfsellemdc  13374
  Copyright terms: Public domain W3C validator