Theorem 0ex 4211

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 4210. (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.

Step	Hyp	Ref	Expression
1		ax-nul 4210	. . 3 ⊢ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥
2		eq0 3510	. . . 4 ⊢ (𝑥 = ∅ ↔ ∀𝑦 ¬ 𝑦 ∈ 𝑥)
3	2	exbii 1651	. . 3 ⊢ (∃𝑥 𝑥 = ∅ ↔ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥)
4	1, 3	mpbir 146	. 2 ⊢ ∃𝑥 𝑥 = ∅
5	4	issetri 2809	1 ⊢ ∅ ∈ V

Syntax hints:  ¬ wn 3  ∀wal 1393   = wceq 1395  ∃wex 1538   ∈ wcel 2200  Vcvv 2799  ∅c0 3491

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 617  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-nul 4210

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-dif 3199  df-nul 3492

This theorem is referenced by:  0elpw  4248  0nep0  4249  iin0r  4253  intv  4254  snexprc  4270  p0ex  4272  undifexmid  4277  exmidexmid  4280  ss1o0el1  4281  exmidsssn  4286  exmidel  4289  exmidundif  4290  exmidundifim  4291  exmid1stab  4292  0elon  4483  onm  4492  ordtriexmidlem2  4612  ordtriexmid  4613  ontriexmidim  4614  ordtri2orexmid  4615  ontr2exmid  4617  onsucsssucexmid  4619  onsucelsucexmidlem1  4620  onsucelsucexmid  4622  regexmidlem1  4625  reg2exmidlema  4626  ordsoexmid  4654  0elsucexmid  4657  ordpwsucexmid  4662  ordtri2or2exmid  4663  ontri2orexmidim  4664  dcextest  4673  peano1  4686  finds  4692  finds2  4693  0elnn  4711  opthprc  4770  nfunv  5351  fun0  5379  acexmidlema  5998  acexmidlemb  5999  acexmidlemab  6001  ovprc  6043  1st0  6296  2nd0  6297  brtpos0  6404  reldmtpos  6405  tfr0dm  6474  rdg0  6539  frec0g  6549  2oex  6585  1n0  6586  el1o  6591  0lt2o  6595  fnom  6604  omexg  6605  om0  6612  nnsucsssuc  6646  mapdm0  6818  map0e  6841  0elixp  6884  en0  6955  ensn1  6956  en1  6959  2dom  6966  map1  6973  rex2dom  6979  dom1o  6985  xp1en  6990  endisj  6991  dom0  7007  php5dom  7032  ssfilem  7045  ssfiexmid  7046  domfiexmid  7048  diffitest  7057  ac6sfi  7068  exmidpw  7081  exmidpw2en  7085  unfiexmid  7091  fi0  7153  djuexb  7222  djulclr  7227  djulcl  7229  djulclb  7233  djulf1or  7234  djulf1o  7236  inl11  7243  djuss  7248  1stinl  7252  2ndinl  7253  0ct  7285  finomni  7318  exmidomni  7320  pr2cv1  7379  exmidonfinlem  7382  exmidfodomrlemr  7391  exmidfodomrlemrALT  7392  exmidaclem  7401  dju0en  7407  djucomen  7409  djuassen  7410  xpdjuen  7411  pw1dom2  7423  pw1ne1  7425  fmelpw1o  7443  indpi  7540  frecfzennn  10660  fihashen1  11033  hashunlem  11038  zfz1iso  11076  lswex  11136  s1prc  11171  ccat1st1st  11187  swrdval  11195  swrd0g  11207  pfxval  11221  pfx0g  11223  fnpfx  11224  swrdccat3blem  11286  ennnfonelemj0  12987  ennnfonelem0  12991  ennnfonelemhom  13001  strsl0  13096  fnpr2ob  13388  xpsfrnel  13392  0g0  13424  gsum0g  13444  topgele  14718  en1top  14766  sn0topon  14777  sn0cld  14826  rest0  14868  restsn  14869  0met  15073  vtxval0  15869  iedgval0  15870  uhgr0  15900  upgr0eop  15937  djulclALT  16220  bj-charfun  16225  bj-d0clsepcl  16343  bj-indint  16349  bj-bdfindis  16365  bj-inf2vnlem1  16388  pw1map  16420  pwle2  16423  pw1nct  16428  0nninf  16430  nninfsellemdc  16436  nnnninfex  16448