Theorem 0ex 5015

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 5014. (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 5014	. . 3 ⊢ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥
2		eq0 4159	. . . 4 ⊢ (𝑥 = ∅ ↔ ∀𝑦 ¬ 𝑦 ∈ 𝑥)
3	2	exbii 1949	. . 3 ⊢ (∃𝑥 𝑥 = ∅ ↔ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥)
4	1, 3	mpbir 223	. 2 ⊢ ∃𝑥 𝑥 = ∅
5	4	issetri 3428	1 ⊢ ∅ ∈ V

Syntax hints:  ¬ wn 3  ∀wal 1656   = wceq 1658  ∃wex 1880   ∈ wcel 2166  Vcvv 3415  ∅c0 4145

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2804  ax-nul 5014

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2813  df-cleq 2819  df-clel 2822  df-nfc 2959  df-v 3417  df-dif 3802  df-nul 4146

This theorem is referenced by:  al0ssb  5016  sseliALT  5017  csbexg  5018  unisn2  5020  class2set  5055  0elpw  5057  0nep0  5059  unidif0  5061  iin0  5062  notzfaus  5063  intv  5064  snexALT  5083  p0ex  5084  dtruALT  5088  zfpair  5126  snex  5130  dtruALT2  5133  opex  5154  opthwiener  5201  0sn0ep  5260  opthprc  5401  nrelv  5459  dmsnsnsn  5855  0elon  6017  nsuceq0  6044  snsn0non  6082  iotaex  6104  nfunv  6157  fun0  6188  fvrn0  6462  fvssunirn  6463  fprg  6674  ovima0  7074  onint0  7258  tfinds2  7325  finds  7354  finds2  7356  xpexr  7369  soex  7372  supp0  7565  fvn0elsupp  7576  fvn0elsuppb  7577  brtpos0  7625  reldmtpos  7626  tfrlem16  7756  tz7.44-1  7769  seqomlem1  7812  1n0  7843  el1o  7847  om0  7865  mapdm0  8138  map0eOLD  8162  ixpexg  8200  0elixp  8207  en0  8286  ensn1  8287  en1  8290  2dom  8296  map1  8306  xp1en  8316  endisj  8317  pw2eng  8336  map2xp  8400  limensuci  8406  1sdom  8433  unxpdom2  8438  sucxpdom  8439  isinf  8443  ac6sfi  8474  fodomfi  8509  0fsupp  8567  fi0  8596  oiexg  8710  brwdom  8742  brwdom2  8748  inf3lemb  8800  infeq5i  8811  dfom3  8822  cantnfvalf  8840  cantnfval2  8844  cantnfle  8846  cantnflt  8847  cantnff  8849  cantnf0  8850  cantnfp1lem1  8853  cantnfp1lem2  8854  cantnfp1lem3  8855  cantnfp1  8856  cantnflem1a  8860  cantnflem1d  8863  cantnflem1  8864  cantnflem3  8866  cantnf  8868  cnfcomlem  8874  cnfcom  8875  cnfcom2lem  8876  cnfcom3  8879  tc0  8901  r10  8909  scottex  9026  djulcl  9050  djulf1o  9052  djuss  9060  djuun  9066  1stinl  9067  2ndinl  9068  infxpenlem  9150  fseqenlem1  9161  uncdadom  9309  cdaun  9310  cdaen  9311  cda1dif  9314  pm110.643  9315  cda0en  9317  cdacomen  9319  cdaassen  9320  xpcdaen  9321  mapcdaen  9322  cdaxpdom  9327  cdainf  9330  infcda1  9331  pwsdompw  9342  pwcdadom  9354  ackbij1lem14  9371  ackbij2lem2  9378  ackbij2lem3  9379  cf0  9389  cfeq0  9394  cfsuc  9395  cflim2  9401  isfin5  9437  isfin4-3  9453  fin1a2lem11  9548  fin1a2lem12  9549  fin1a2lem13  9550  axcc2lem  9574  ac6num  9617  zornn0g  9643  ttukeylem3  9649  brdom3  9666  iundom2g  9678  cardeq0  9690  alephadd  9715  pwcfsdom  9721  axpowndlem3  9737  canthwe  9789  canthp1lem1  9790  pwxpndom2  9803  pwcdandom  9805  gchxpidm  9807  intwun  9873  0tsk  9893  grothomex  9967  indpi  10045  fzennn  13063  hash0  13449  hashen1  13451  hashmap  13512  hashbc  13527  hashf1  13531  hashge3el3dif  13558  ccat1st1st  13689  swrdval  13704  swrd00  13705  swrd0  13724  cshfn  13909  cshfnOLD  13910  cshnz  13912  cshnzOLD  13913  0csh0  13914  0csh0OLD  13915  incexclem  14943  incexc  14944  rexpen  15332  sadcf  15549  sadc0  15550  sadcp1  15551  smupf  15574  smup0  15575  smupp1  15576  0ram  16096  ram0  16098  cshws0  16175  str0  16275  ressbas  16294  ress0  16298  0rest  16444  xpscg  16572  xpscfn  16573  xpsc0  16574  xpsc1  16575  xpsfrnel  16577  xpsfrnel2  16579  xpsle  16595  ismred2  16617  acsfn  16673  0cat  16702  ciclcl  16815  cicrcl  16816  cicer  16819  setcepi  17091  0pos  17308  meet0  17491  join0  17492  mgm0b  17610  gsum0  17632  sgrp0b  17646  ga0  18082  psgn0fv0  18283  pmtrsn  18291  oppglsm  18409  efgi0  18485  vrgpf  18535  vrgpinv  18536  frgpuptinv  18538  frgpup2  18543  0frgp  18546  frgpnabllem1  18630  frgpnabllem2  18631  dprd0  18785  dmdprdpr  18803  dprdpr  18804  00lsp  19341  fvcoe1  19938  coe1f2  19940  coe1sfi  19944  coe1add  19995  coe1mul2lem1  19998  coe1mul2lem2  19999  coe1mul2  20000  ply1coe  20027  evls1rhmlem  20047  evl1sca  20059  evl1var  20061  pf1mpf  20077  pf1ind  20080  cnfldfunALT  20120  frgpcyg  20282  frlmiscvec  20556  mat0dimscm  20644  mat0dimcrng  20645  mat0scmat  20713  mavmul0  20727  mavmul0g  20728  mvmumamul1  20729  mdet0pr  20767  mdet0f1o  20768  mdet0fv0  20769  mdetunilem9  20795  d0mat2pmat  20914  chpmat0d  21010  topgele  21106  en1top  21160  en2top  21161  sn0topon  21174  indistopon  21177  indistps  21187  indistps2  21188  sn0cld  21266  indiscld  21267  neipeltop  21305  rest0  21345  restsn  21346  cmpfi  21583  refun0  21690  txindislem  21808  hmphindis  21972  xpstopnlem1  21984  xpstopnlem2  21986  ptcmpfi  21988  snfil  22039  fbasfip  22043  fgcl  22053  filconn  22058  fbasrn  22059  cfinfil  22068  csdfil  22069  supfil  22070  ufildr  22106  fin1aufil  22107  rnelfmlem  22127  fclsval  22183  tmdgsum  22270  tsmsfbas  22302  ust0  22394  ustn0  22395  0met  22542  xpsdsval  22557  minveclem3b  23597  tdeglem2  24221  deg1ldg  24252  deg1leb  24255  deg1val  24256  ulm0  24545  uhgr0  26372  upgr0eop  26413  upgr0eopALT  26415  usgr0  26541  usgr0eop  26544  lfuhgr1v0e  26552  griedg0prc  26562  0grsubgr  26576  cplgr0  26724  0grrusgr  26878  clwwlk0on0  27466  0ewlk  27491  0wlkon  27497  0trlon  27501  0pthon  27504  0pthonv  27506  0conngr  27569  konigsberglem1  27632  konigsberglem2  27633  konigsberglem3  27634  wlkl0  27771  disjdifprg  29936  disjun0  29956  fpwrelmapffslem  30056  f1ocnt  30107  resvsca  30376  locfinref  30454  esumnul  30656  esumrnmpt2  30676  prsiga  30740  ldsysgenld  30769  ldgenpisyslem1  30772  oms0  30905  carsggect  30926  eulerpartgbij  30980  eulerpartlemmf  30983  repr0  31239  breprexp  31261  bnj941  31390  bnj97  31483  bnj149  31492  bnj150  31493  bnj944  31555  derang0  31698  indispconn  31763  rdgprc  32239  dfrdg3  32241  trpredpred  32267  trpred0  32275  nosgnn0  32351  nodense  32382  nolt02o  32385  nulsslt  32448  nulssgt  32449  fullfunfnv  32593  fullfunfv  32594  rank0  32817  ssoninhaus  32981  onint1  32982  bj-0nel1  33463  bj-xpnzex  33469  bj-eltag  33488  bj-0eltag  33489  bj-tagss  33491  bj-pr1val  33515  bj-nuliota  33542  bj-nuliotaALT  33543  bj-rest10  33565  bj-rest10b  33566  bj-rest0  33570  finxpreclem1  33772  finxpreclem2  33773  finxp0  33774  finxpreclem5  33778  cnfin0  33786  cnfinltrel  33787  lindsadd  33947  poimirlem28  33982  heibor1lem  34151  heiborlem6  34158  reheibor  34181  n0elqs  34647  mzpcompact2lem  38159  wopprc  38441  pw2f1ocnv  38448  pwslnmlem0  38505  pwfi2f1o  38510  relintabex  38729  clsk1indlem0  39180  clsk1indlem4  39183  clsk1indlem1  39184  fnchoice  40007  eliuniincex  40108  mapdm0OLD  40192  limsup0  40722  0cnv  40770  liminf0  40821  0cnf  40886  dvnprodlem3  40959  qndenserrnbl  41307  prsal  41330  intsal  41340  sge00  41385  sge0sn  41388  nnfoctbdjlem  41464  isomenndlem  41539  hoiqssbl  41634  ovnsubadd2lem  41654  iota0def  41970  aiota0def  41992  afv0fv0  42052  lincval0  43052  lco0  43064  linds0  43102  bnd2d  43324