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

Theorem 0ex 3943
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 3942. (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 3942 . . 3 𝑥𝑦 ¬ 𝑦𝑥
2 eq0 3290 . . . 4 (𝑥 = ∅ ↔ ∀𝑦 ¬ 𝑦𝑥)
32exbii 1539 . . 3 (∃𝑥 𝑥 = ∅ ↔ ∃𝑥𝑦 ¬ 𝑦𝑥)
41, 3mpbir 144 . 2 𝑥 𝑥 = ∅
54issetri 2622 1 ∅ ∈ V
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wal 1285   = wceq 1287  wex 1424  wcel 1436  Vcvv 2615  c0 3275
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067  ax-nul 3942
This theorem depends on definitions:  df-bi 115  df-tru 1290  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-v 2617  df-dif 2990  df-nul 3276
This theorem is referenced by:  0elpw  3976  0nep0  3977  iin0r  3981  intv  3982  snexprc  3997  p0ex  3999  undifexmid  4004  exmidexmid  4007  exmid01  4008  exmidel  4010  exmidundif  4011  0elon  4195  onm  4204  ordtriexmidlem2  4312  ordtriexmid  4313  ordtri2orexmid  4314  ontr2exmid  4316  onsucsssucexmid  4318  onsucelsucexmidlem1  4319  onsucelsucexmid  4321  regexmidlem1  4324  reg2exmidlema  4325  ordsoexmid  4353  0elsucexmid  4356  ordpwsucexmid  4361  ordtri2or2exmid  4362  dcextest  4371  peano1  4384  finds  4390  finds2  4391  0elnn  4407  opthprc  4459  nfunv  5014  fun0  5039  acexmidlema  5606  acexmidlemb  5607  acexmidlemab  5609  ovprc  5643  1st0  5874  2nd0  5875  brtpos0  5973  reldmtpos  5974  tfr0dm  6043  rdg0  6108  frec0g  6118  1n0  6153  el1o  6157  fnom  6167  omexg  6168  om0  6175  nnsucsssuc  6209  mapdm0  6374  map0e  6397  en0  6466  ensn1  6467  en1  6470  2dom  6476  map1  6483  xp1en  6493  endisj  6494  dom0  6508  php5dom  6533  ssfilem  6545  ssfiexmid  6546  domfiexmid  6548  diffitest  6557  ac6sfi  6568  exmidpw  6578  unfiexmid  6582  djulclr  6688  djulcl  6690  djulclb  6694  djulf1or  6695  djulf1o  6697  djur  6704  djuss  6708  1stinl  6712  2ndinl  6713  finomni  6743  exmidomni  6745  fodjuomnilemf  6747  exmidfodomrlemr  6775  exmidfodomrlemrALT  6776  indpi  6848  frecfzennn  9764  fihashen1  10125  hashunlem  10130  zfz1iso  10164  djulclALT  11189  bj-d0clsepcl  11308  bj-indint  11314  bj-bdfindis  11330  bj-inf2vnlem1  11353  0lt2o  11373  pw1dom2  11377  0nninf  11381  nninfsellemdc  11390
  Copyright terms: Public domain W3C validator