Theorem 0ex 4242

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

Syntax hints:  ¬ wn 3  ∀wal 1396   = wceq 1398  ∃wex 1541   ∈ wcel 2205  Vcvv 2815  ∅c0 3512

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 2216  ax-nul 4241

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-v 2817  df-dif 3216  df-nul 3513

This theorem is referenced by:  0elpw  4282  0nep0  4283  iin0r  4287  intv  4288  snexprc  4304  p0ex  4306  undifexmid  4311  exmidexmid  4314  ss1o0el1  4315  exmidsssn  4320  exmidel  4323  exmidundif  4324  exmidundifim  4325  exmid1stab  4326  0elon  4518  onm  4527  ordtriexmidlem2  4647  ordtriexmid  4648  ontriexmidim  4649  ordtri2orexmid  4650  ontr2exmid  4652  onsucsssucexmid  4654  onsucelsucexmidlem1  4655  onsucelsucexmid  4657  regexmidlem1  4660  reg2exmidlema  4661  ordsoexmid  4689  0elsucexmid  4692  ordpwsucexmid  4697  ordtri2or2exmid  4698  ontri2orexmidim  4699  dcextest  4708  peano1  4721  finds  4727  finds2  4728  0elnn  4746  opthprc  4806  nfunv  5390  fun0  5419  acexmidlema  6049  acexmidlemb  6050  acexmidlemab  6052  ovprc  6094  1st0  6351  2nd0  6352  supp0  6451  fvn0elsupp  6464  fvn0elsuppb  6465  brtpos0  6496  reldmtpos  6497  tfr0dm  6566  rdg0  6631  frec0g  6641  2oex  6677  1n0  6678  el1o  6683  0lt2o  6687  fnom  6696  omexg  6697  om0  6704  nnsucsssuc  6738  mapdm0  6910  map0e  6933  0elixp  6977  en0  7048  ensn1  7049  en1  7052  2dom  7059  map1  7067  rex2dom  7076  dom1o  7082  xp1en  7087  endisj  7088  dom0  7104  php5dom  7130  ssfilem  7143  ssfiexmid  7144  ssfilemd  7145  ssfiexmidt  7146  domfiexmid  7148  diffitest  7157  ac6sfi  7168  exmidpw  7181  exmidpw2en  7185  unfiexmid  7191  mapfi  7227  0fsupp  7264  fi0  7275  djuexb  7348  djulclr  7353  djulcl  7355  djulclb  7359  djulf1or  7360  djulf1o  7362  inl11  7369  djuss  7374  1stinl  7378  2ndinl  7379  0ct  7411  finomni  7444  exmidomni  7446  pr2cv1  7505  exmidonfinlem  7509  exmidfodomrlemr  7518  exmidfodomrlemrALT  7519  exmidaclem  7528  dju0en  7534  djucomen  7536  djuassen  7537  xpdjuen  7538  pw1dom2  7550  pw1ne1  7552  indpi  7673  frecfzennn  10812  fihashen1  11187  hashunlem  11193  hashmap  11217  hashfibc  11232  zfz1iso  11238  lswex  11301  s1prc  11336  ccat1st1st  11354  swrdval  11365  swrd0g  11377  pfxval  11391  pfx0g  11393  fnpfx  11394  swrdccat3blem  11456  fzf1o  12086  ennnfonelemj0  13236  ennnfonelem0  13240  ennnfonelemhom  13250  strsl0  13345  fnpr2ob  13604  xpsfrnel  13608  0g0  13639  gsum0g  13659  topgele  15020  en1top  15068  sn0topon  15079  sn0cld  15128  rest0  15170  restsn  15171  0met  15375  vtxval0  16174  iedgval0  16175  uhgr0  16206  upgr0eop  16243  usgr0  16360  usgr0eop  16363  griedg0prc  16371  0grsubgr  16385  clwwlk0on0  16552  konigsberglem1  16609  konigsberglem2  16610  konigsberglem3  16611  djulclALT  16699  bj-charfun  16703  bj-d0clsepcl  16821  bj-indint  16827  bj-bdfindis  16843  bj-inf2vnlem1  16866  pw1map  16895  pwle2  16898  pw1nct  16903  0nninf  16908  nninfsellemdc  16914  nnnninfex  16926