Theorem 0ex 4131

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

Syntax hints:  ¬ wn 3  ∀wal 1351   = wceq 1353  ∃wex 1492   ∈ wcel 2148  Vcvv 2738  ∅c0 3423

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 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-nul 4130

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2740  df-dif 3132  df-nul 3424

This theorem is referenced by:  0elpw  4165  0nep0  4166  iin0r  4170  intv  4171  snexprc  4187  p0ex  4189  undifexmid  4194  exmidexmid  4197  ss1o0el1  4198  exmidsssn  4203  exmidel  4206  exmidundif  4207  exmidundifim  4208  exmid1stab  4209  0elon  4393  onm  4402  ordtriexmidlem2  4520  ordtriexmid  4521  ontriexmidim  4522  ordtri2orexmid  4523  ontr2exmid  4525  onsucsssucexmid  4527  onsucelsucexmidlem1  4528  onsucelsucexmid  4530  regexmidlem1  4533  reg2exmidlema  4534  ordsoexmid  4562  0elsucexmid  4565  ordpwsucexmid  4570  ordtri2or2exmid  4571  ontri2orexmidim  4572  dcextest  4581  peano1  4594  finds  4600  finds2  4601  0elnn  4619  opthprc  4678  nfunv  5250  fun0  5275  acexmidlema  5866  acexmidlemb  5867  acexmidlemab  5869  ovprc  5910  1st0  6145  2nd0  6146  brtpos0  6253  reldmtpos  6254  tfr0dm  6323  rdg0  6388  frec0g  6398  1n0  6433  el1o  6438  0lt2o  6442  fnom  6451  omexg  6452  om0  6459  nnsucsssuc  6493  mapdm0  6663  map0e  6686  0elixp  6729  en0  6795  ensn1  6796  en1  6799  2dom  6805  map1  6812  xp1en  6823  endisj  6824  dom0  6838  php5dom  6863  ssfilem  6875  ssfiexmid  6876  domfiexmid  6878  diffitest  6887  ac6sfi  6898  exmidpw  6908  unfiexmid  6917  fi0  6974  djuexb  7043  djulclr  7048  djulcl  7050  djulclb  7054  djulf1or  7055  djulf1o  7057  inl11  7064  djuss  7069  1stinl  7073  2ndinl  7074  0ct  7106  finomni  7138  exmidomni  7140  exmidonfinlem  7192  exmidfodomrlemr  7201  exmidfodomrlemrALT  7202  exmidaclem  7207  dju0en  7213  djucomen  7215  djuassen  7216  xpdjuen  7217  pw1dom2  7226  pw1ne1  7228  indpi  7341  frecfzennn  10426  fihashen1  10779  hashunlem  10784  zfz1iso  10821  ennnfonelemj0  12402  ennnfonelem0  12406  ennnfonelemhom  12416  strsl0  12511  fnpr2ob  12759  xpsfrnel  12763  0g0  12795  topgele  13532  en1top  13580  sn0topon  13591  sn0cld  13640  rest0  13682  restsn  13683  0met  13887  djulclALT  14556  fmelpw1o  14561  bj-charfun  14562  bj-d0clsepcl  14680  bj-indint  14686  bj-bdfindis  14702  bj-inf2vnlem1  14725  pwle2  14751  pw1nct  14755  0nninf  14756  nninfsellemdc  14762