Theorem 0ex 4132

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

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

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 4131

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 2741  df-dif 3133  df-nul 3425

This theorem is referenced by:  0elpw  4166  0nep0  4167  iin0r  4171  intv  4172  snexprc  4188  p0ex  4190  undifexmid  4195  exmidexmid  4198  ss1o0el1  4199  exmidsssn  4204  exmidel  4207  exmidundif  4208  exmidundifim  4209  exmid1stab  4210  0elon  4394  onm  4403  ordtriexmidlem2  4521  ordtriexmid  4522  ontriexmidim  4523  ordtri2orexmid  4524  ontr2exmid  4526  onsucsssucexmid  4528  onsucelsucexmidlem1  4529  onsucelsucexmid  4531  regexmidlem1  4534  reg2exmidlema  4535  ordsoexmid  4563  0elsucexmid  4566  ordpwsucexmid  4571  ordtri2or2exmid  4572  ontri2orexmidim  4573  dcextest  4582  peano1  4595  finds  4601  finds2  4602  0elnn  4620  opthprc  4679  nfunv  5251  fun0  5276  acexmidlema  5869  acexmidlemb  5870  acexmidlemab  5872  ovprc  5913  1st0  6148  2nd0  6149  brtpos0  6256  reldmtpos  6257  tfr0dm  6326  rdg0  6391  frec0g  6401  1n0  6436  el1o  6441  0lt2o  6445  fnom  6454  omexg  6455  om0  6462  nnsucsssuc  6496  mapdm0  6666  map0e  6689  0elixp  6732  en0  6798  ensn1  6799  en1  6802  2dom  6808  map1  6815  xp1en  6826  endisj  6827  dom0  6841  php5dom  6866  ssfilem  6878  ssfiexmid  6879  domfiexmid  6881  diffitest  6890  ac6sfi  6901  exmidpw  6911  unfiexmid  6920  fi0  6977  djuexb  7046  djulclr  7051  djulcl  7053  djulclb  7057  djulf1or  7058  djulf1o  7060  inl11  7067  djuss  7072  1stinl  7076  2ndinl  7077  0ct  7109  finomni  7141  exmidomni  7143  exmidonfinlem  7195  exmidfodomrlemr  7204  exmidfodomrlemrALT  7205  exmidaclem  7210  dju0en  7216  djucomen  7218  djuassen  7219  xpdjuen  7220  pw1dom2  7229  pw1ne1  7231  indpi  7344  frecfzennn  10429  fihashen1  10782  hashunlem  10787  zfz1iso  10824  ennnfonelemj0  12405  ennnfonelem0  12409  ennnfonelemhom  12419  strsl0  12514  fnpr2ob  12766  xpsfrnel  12770  0g0  12802  topgele  13717  en1top  13765  sn0topon  13776  sn0cld  13825  rest0  13867  restsn  13868  0met  14072  djulclALT  14741  fmelpw1o  14746  bj-charfun  14747  bj-d0clsepcl  14865  bj-indint  14871  bj-bdfindis  14887  bj-inf2vnlem1  14910  pwle2  14937  pw1nct  14941  0nninf  14942  nninfsellemdc  14948