Theorem 0ex 4237

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 4236. (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 4236	. . 3 ⊢ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥
2		eq0 3527	. . . 4 ⊢ (𝑥 = ∅ ↔ ∀𝑦 ¬ 𝑦 ∈ 𝑥)
3	2	exbii 1654	. . 3 ⊢ (∃𝑥 𝑥 = ∅ ↔ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥)
4	1, 3	mpbir 146	. 2 ⊢ ∃𝑥 𝑥 = ∅
5	4	issetri 2823	1 ⊢ ∅ ∈ V

Syntax hints:  ¬ wn 3  ∀wal 1396   = wceq 1398  ∃wex 1541   ∈ wcel 2203  Vcvv 2813  ∅c0 3508

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 619  ax-in2 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214  ax-nul 4236

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-v 2815  df-dif 3213  df-nul 3509

This theorem is referenced by:  0elpw  4277  0nep0  4278  iin0r  4282  intv  4283  snexprc  4299  p0ex  4301  undifexmid  4306  exmidexmid  4309  ss1o0el1  4310  exmidsssn  4315  exmidel  4318  exmidundif  4319  exmidundifim  4320  exmid1stab  4321  0elon  4513  onm  4522  ordtriexmidlem2  4642  ordtriexmid  4643  ontriexmidim  4644  ordtri2orexmid  4645  ontr2exmid  4647  onsucsssucexmid  4649  onsucelsucexmidlem1  4650  onsucelsucexmid  4652  regexmidlem1  4655  reg2exmidlema  4656  ordsoexmid  4684  0elsucexmid  4687  ordpwsucexmid  4692  ordtri2or2exmid  4693  ontri2orexmidim  4694  dcextest  4703  peano1  4716  finds  4722  finds2  4723  0elnn  4741  opthprc  4801  nfunv  5385  fun0  5414  acexmidlema  6041  acexmidlemb  6042  acexmidlemab  6044  ovprc  6086  1st0  6338  2nd0  6339  supp0  6438  fvn0elsupp  6451  fvn0elsuppb  6452  brtpos0  6483  reldmtpos  6484  tfr0dm  6553  rdg0  6618  frec0g  6628  2oex  6664  1n0  6665  el1o  6670  0lt2o  6674  fnom  6683  omexg  6684  om0  6691  nnsucsssuc  6725  mapdm0  6897  map0e  6920  0elixp  6964  en0  7035  ensn1  7036  en1  7039  2dom  7046  map1  7054  rex2dom  7063  dom1o  7069  xp1en  7074  endisj  7075  dom0  7091  php5dom  7117  ssfilem  7130  ssfiexmid  7131  ssfilemd  7132  ssfiexmidt  7133  domfiexmid  7135  diffitest  7144  ac6sfi  7155  exmidpw  7168  exmidpw2en  7172  unfiexmid  7178  mapfi  7214  0fsupp  7251  fi0  7262  djuexb  7335  djulclr  7340  djulcl  7342  djulclb  7346  djulf1or  7347  djulf1o  7349  inl11  7356  djuss  7361  1stinl  7365  2ndinl  7366  0ct  7398  finomni  7431  exmidomni  7433  pr2cv1  7492  exmidonfinlem  7496  exmidfodomrlemr  7505  exmidfodomrlemrALT  7506  exmidaclem  7515  dju0en  7521  djucomen  7523  djuassen  7524  xpdjuen  7525  pw1dom2  7537  pw1ne1  7539  indpi  7657  frecfzennn  10788  fihashen1  11162  hashunlem  11168  hashmap  11192  hashfibc  11207  zfz1iso  11213  lswex  11276  s1prc  11311  ccat1st1st  11329  swrdval  11340  swrd0g  11352  pfxval  11366  pfx0g  11368  fnpfx  11369  swrdccat3blem  11431  fzf1o  12061  ennnfonelemj0  13152  ennnfonelem0  13156  ennnfonelemhom  13166  strsl0  13261  fnpr2ob  13553  xpsfrnel  13557  0g0  13589  gsum0g  13609  topgele  14894  en1top  14942  sn0topon  14953  sn0cld  15002  rest0  15044  restsn  15045  0met  15249  vtxval0  16048  iedgval0  16049  uhgr0  16080  upgr0eop  16117  usgr0  16234  usgr0eop  16237  griedg0prc  16245  0grsubgr  16259  clwwlk0on0  16426  konigsberglem1  16483  konigsberglem2  16484  konigsberglem3  16485  djulclALT  16573  bj-charfun  16577  bj-d0clsepcl  16695  bj-indint  16701  bj-bdfindis  16717  bj-inf2vnlem1  16740  pw1map  16769  pwle2  16772  pw1nct  16777  0nninf  16782  nninfsellemdc  16788  nnnninfex  16800