Theorem 0ex 5203

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 5202. (Contributed by NM, 21-Jun-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 5202	. . 3 ⊢ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥
2		eq0 4307	. . . 4 ⊢ (𝑥 = ∅ ↔ ∀𝑦 ¬ 𝑦 ∈ 𝑥)
3	2	exbii 1844	. . 3 ⊢ (∃𝑥 𝑥 = ∅ ↔ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥)
4	1, 3	mpbir 233	. 2 ⊢ ∃𝑥 𝑥 = ∅
5	4	issetri 3510	1 ⊢ ∅ ∈ V

Syntax hints:  ¬ wn 3  ∀wal 1531   = wceq 1533  ∃wex 1776   ∈ wcel 2110  Vcvv 3494  ∅c0 4290

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-11 2157  ax-12 2173  ax-ext 2793  ax-nul 5202

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-dif 3938  df-nul 4291

This theorem is referenced by:  al0ssb  5204  sseliALT  5205  csbexg  5206  unisn2  5208  class2set  5246  0elpw  5248  0nep0  5250  unidif0  5252  iin0  5253  notzfaus  5254  notzfausOLD  5255  intv  5256  snexALT  5275  p0ex  5276  dtruALT  5280  zfpair  5313  snex  5323  dtruALT2  5327  opex  5348  opthwiener  5396  0sn0ep  5464  opthprc  5610  nrelv  5667  dmsnsnsn  6071  0elon  6238  nsuceq0  6265  snsn0non  6303  iotaex  6329  fun0  6413  fvrn0  6692  fvssunirn  6693  fprg  6911  ovima0  7321  onint0  7505  tfinds2  7572  finds  7602  finds2  7604  xpexr  7617  soex  7620  supp0  7829  fvn0elsupp  7840  fvn0elsuppb  7841  brtpos0  7893  reldmtpos  7894  tfrlem16  8023  tz7.44-1  8036  seqomlem1  8080  1n0  8113  el1o  8118  om0  8136  mapdm0  8415  0map0sn0  8443  ixpexg  8480  0elixp  8487  en0  8566  ensn1  8567  en1  8570  2dom  8576  map1  8586  xp1en  8597  endisj  8598  pw2eng  8617  map2xp  8681  limensuci  8687  1sdom  8715  unxpdom2  8720  sucxpdom  8721  isinf  8725  ac6sfi  8756  fodomfi  8791  0fsupp  8849  fi0  8878  oiexg  8993  brwdom  9025  brwdom2  9031  inf3lemb  9082  infeq5i  9093  dfom3  9104  cantnfvalf  9122  cantnfval2  9126  cantnfle  9128  cantnflt  9129  cantnff  9131  cantnf0  9132  cantnfp1lem1  9135  cantnfp1lem3  9137  cantnfp1  9138  cantnflem1a  9142  cantnflem1d  9145  cantnflem1  9146  cantnf  9150  cnfcomlem  9156  cnfcom  9157  cnfcom2lem  9158  cnfcom3  9161  tc0  9183  r10  9191  scottex  9308  djulcl  9333  djulf1o  9335  djuss  9343  djuun  9349  1stinl  9350  2ndinl  9351  infxpenlem  9433  fseqenlem1  9444  undjudom  9587  endjudisj  9588  djuen  9589  dju1dif  9592  dju1p1e2  9593  dju0en  9595  djucomen  9597  djuassen  9598  xpdjuen  9599  mapdjuen  9600  djuxpdom  9605  djuinf  9608  infdju1  9609  djulepw  9612  pwsdompw  9620  pwdjudom  9632  ackbij1lem14  9649  ackbij2lem2  9656  ackbij2lem3  9657  cf0  9667  cfeq0  9672  cfsuc  9673  cflim2  9679  isfin5  9715  isfin4p1  9731  fin1a2lem11  9826  fin1a2lem12  9827  fin1a2lem13  9828  axcc2lem  9852  ac6num  9895  zornn0g  9921  ttukeylem3  9927  brdom3  9944  iundom2g  9956  cardeq0  9968  pwcfsdom  9999  axpowndlem3  10015  canthwe  10067  canthp1lem1  10068  pwxpndom2  10081  pwdjundom  10083  gchxpidm  10085  intwun  10151  0tsk  10171  grothomex  10245  indpi  10323  fzennn  13330  hash0  13722  hashen1  13725  hashmap  13790  hashbc  13805  hashf1  13809  hashge3el3dif  13838  ccat1st1st  13978  swrdval  13999  swrd00  14000  swrd0  14014  cshfn  14146  cshnz  14148  0csh0  14149  incexclem  15185  incexc  15186  rexpen  15575  sadcf  15796  sadc0  15797  sadcp1  15798  smupf  15821  smup0  15822  smupp1  15823  0ram  16350  ram0  16352  cshws0  16429  str0  16529  ressbas  16548  ress0  16552  0rest  16697  fnpr2ob  16825  xpsfrnel  16829  xpsle  16846  ismred2  16868  acsfn  16924  0cat  16953  ciclcl  17066  cicrcl  17067  cicer  17070  setcepi  17342  0pos  17558  meet0  17741  join0  17742  mgm0b  17861  gsum0  17888  sgrp0b  17903  efmnd0nmnd  18049  pwmnd  18096  mulgfval  18220  ga0  18422  psgn0fv0  18633  pmtrsn  18641  oppglsm  18761  efgi0  18840  vrgpf  18888  vrgpinv  18889  frgpuptinv  18891  frgpup2  18896  0frgp  18899  frgpnabllem1  18987  frgpnabllem2  18988  dprd0  19147  dmdprdpr  19165  dprdpr  19166  00lsp  19747  fvcoe1  20369  coe1f2  20371  coe1sfi  20375  coe1add  20426  coe1mul2lem1  20429  coe1mul2lem2  20430  coe1mul2  20431  ply1coe  20458  evls1rhmlem  20478  evl1sca  20491  evl1var  20493  pf1mpf  20509  pf1ind  20512  cnfldfunALT  20552  frgpcyg  20714  frlmiscvec  20987  mat0dimscm  21072  mat0dimcrng  21073  mat0scmat  21141  mavmul0  21155  mavmul0g  21156  mvmumamul1  21157  mdet0pr  21195  mdet0f1o  21196  mdet0fv0  21197  mdetunilem9  21223  d0mat2pmat  21340  chpmat0d  21436  en1top  21586  en2top  21587  sn0topon  21600  indistopon  21603  indistps  21613  indistps2  21614  sn0cld  21692  indiscld  21693  neipeltop  21731  rest0  21771  restsn  21772  cmpfi  22010  refun0  22117  txindislem  22235  hmphindis  22399  xpstopnlem1  22411  xpstopnlem2  22413  ptcmpfi  22415  snfil  22466  fbasfip  22470  fgcl  22480  filconn  22485  fbasrn  22486  cfinfil  22495  csdfil  22496  supfil  22497  ufildr  22533  fin1aufil  22534  rnelfmlem  22554  fclsval  22610  tmdgsum  22697  tsmsfbas  22730  ust0  22822  ustn0  22823  0met  22970  xpsdsval  22985  minveclem3b  24025  tdeglem2  24649  deg1ldg  24680  deg1leb  24683  deg1val  24684  ulm0  24973  uhgr0  26852  upgr0eop  26893  upgr0eopALT  26895  usgr0  27019  usgr0eop  27022  lfuhgr1v0e  27030  griedg0prc  27040  0grsubgr  27054  cplgr0  27201  0grrusgr  27355  clwwlk0on0  27865  0ewlk  27887  0wlkon  27893  0trlon  27897  0pthon  27900  0pthonv  27902  0conngr  27965  konigsberglem1  28025  konigsberglem2  28026  konigsberglem3  28027  wlkl0  28140  disjdifprg  30319  disjun0  30339  fpwrelmapffslem  30462  f1ocnt  30519  resvsca  30898  locfinref  31100  esumnul  31302  esumrnmpt2  31322  prsiga  31385  ldsysgenld  31414  ldgenpisyslem1  31417  oms0  31550  carsggect  31571  eulerpartgbij  31625  eulerpartlemmf  31628  repr0  31877  breprexp  31899  bnj941  32039  bnj97  32133  bnj149  32142  bnj150  32143  bnj944  32205  derang0  32411  indispconn  32476  goeleq12bg  32591  satf0  32614  satf0op  32619  fmla0  32624  fmla0xp  32625  fmlasuc0  32626  fmlafvel  32627  fmlasuc  32628  fmlaomn0  32632  fmla0disjsuc  32640  satfdmfmla  32642  satfv0fvfmla0  32655  sate0  32657  sate0fv0  32659  sategoelfvb  32661  ex-sategoelel  32663  prv0  32672  prv1n  32673  rdgprc  33034  dfrdg3  33036  trpredpred  33062  trpred0  33070  nosgnn0  33160  nodense  33191  nolt02o  33194  nulsslt  33257  nulssgt  33258  fullfunfnv  33402  fullfunfv  33403  rank0  33626  ssoninhaus  33791  onint1  33792  bj-0nel1  34260  bj-xpnzex  34266  bj-eltag  34284  bj-0eltag  34285  bj-tagss  34287  bj-pr1val  34311  bj-nuliota  34344  bj-nuliotaALT  34345  bj-rest10  34373  bj-rest10b  34374  bj-rest0  34378  rdgssun  34653  finxpreclem1  34664  finxpreclem2  34665  finxp0  34666  finxpreclem5  34670  poimirlem28  34914  heibor1lem  35081  heiborlem6  35088  reheibor  35111  n0elqs  35577  mzpcompact2lem  39341  wopprc  39620  pw2f1ocnv  39627  pwslnmlem0  39684  pwfi2f1o  39689  clsk1indlem0  40384  clsk1indlem4  40387  clsk1indlem1  40388  mnupwd  40596  mnuprdlem1  40601  mnuprdlem2  40602  mnuprdlem3  40603  mnurnd  40612  fnchoice  41279  eliuniincex  41368  limsup0  41968  0cnv  42016  liminf0  42067  0cnf  42153  dvnprodlem3  42226  qndenserrnbl  42574  prsal  42597  intsal  42607  sge00  42652  sge0sn  42655  nnfoctbdjlem  42731  isomenndlem  42806  hoiqssbl  42901  ovnsubadd2lem  42921  iota0def  43267  aiota0def  43288  afv0fv0  43342  0nelsetpreimafv  43544  lincval0  44464  lco0  44476  linds0  44514  bnd2d  44778