MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  0ex Unicode version

Theorem 0ex 4124
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 4123. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)
Assertion
Ref Expression
0ex  |-  (/)  e.  _V

Proof of Theorem 0ex
StepHypRef Expression
1 ax-nul 4123 . . 3  |-  E. x A. y  -.  y  e.  x
2 eq0 3444 . . . 4  |-  ( x  =  (/)  <->  A. y  -.  y  e.  x )
32exbii 1580 . . 3  |-  ( E. x  x  =  (/)  <->  E. x A. y  -.  y  e.  x )
41, 3mpbir 202 . 2  |-  E. x  x  =  (/)
54issetri 2770 1  |-  (/)  e.  _V
Colors of variables: wff set class
Syntax hints:   -. wn 5   A.wal 1532   E.wex 1537    = wceq 1619    e. wcel 1621   _Vcvv 2763   (/)c0 3430
This theorem is referenced by:  class2set  4150  0elpw  4152  0nep0  4153  unidif0  4155  iin0  4156  notzfaus  4157  intv  4158  snexALT  4168  p0ex  4169  dtruALT  4179  zfpair  4184  snex  4188  dtruALT2  4191  opex  4209  opthwiener  4240  0elon  4417  nsuceq0  4444  snsn0non  4483  unisn2  4494  onint0  4559  tfinds2  4626  finds  4654  finds2  4656  opthprc  4724  xpexr  5102  soex  5110  dmsnsnsn  5138  nfunv  5224  fun0  5245  fvrn0  5484  fvssunirn  5485  brtpos0  6175  reldmtpos  6176  iotaex  6242  tfrlem16  6377  tz7.44-1  6387  seqomlem1  6430  1n0  6462  el1o  6466  om0  6484  map0e  6773  ixpexg  6808  0elixp  6815  en0  6892  ensn1  6893  en1  6896  2dom  6901  map1  6907  xp1en  6916  endisj  6917  pw2eng  6936  map2xp  6999  limensuci  7005  1sdom  7033  unxpdom2  7039  sucxpdom  7040  isinf  7044  ac6sfi  7069  fodomfi  7103  fi0  7141  oiexg  7218  brwdom  7249  brwdom2  7255  inf3lemb  7294  infeq5i  7305  dfom3  7316  cantnfvalf  7334  cantnfval2  7338  cantnflt  7341  cantnff  7343  cantnf0  7344  cantnfp1lem3  7350  cantnflem1d  7358  cantnflem1  7359  cantnf  7363  cnfcom  7371  tc0  7400  r10  7408  scottex  7523  infxpenlem  7609  fseqenlem1  7619  dfac9  7730  uncdadom  7765  cdaun  7766  cdaen  7767  cda1dif  7770  pm110.643  7771  cda0en  7773  cdacomen  7775  cdaassen  7776  xpcdaen  7777  mapcdaen  7778  cdaxpdom  7783  cdainf  7786  infcda1  7787  pwsdompw  7798  pwcdadom  7810  ackbij1lem14  7827  ackbij2lem2  7834  ackbij2lem3  7835  cf0  7845  cfeq0  7850  cfsuc  7851  cflim2  7857  isfin5  7893  isfin4-3  7909  fin1a2lem11  8004  fin1a2lem12  8005  fin1a2lem13  8006  axcc2lem  8030  ac6num  8074  zornn0g  8100  ttukeylem3  8106  brdom3  8121  iundom2g  8130  cardeq0  8142  alephadd  8167  pwcfsdom  8173  axpowndlem3  8189  canthwe  8241  canthp1lem1  8242  pwxpndom2  8255  pwcdandom  8257  gchxpidm  8259  intwun  8325  0tsk  8345  grothomex  8419  indpi  8499  fzennn  10996  hash0  11321  hashmap  11352  hashbc  11356  hashf1  11360  swrdval  11415  swrd00  11416  rexpen  12468  sadcf  12606  sadc0  12607  sadcp1  12608  smupf  12631  smup0  12632  smupp1  12633  0ram  13029  ram0  13031  str0  13146  ressbas  13160  ress0  13164  0rest  13296  xpscg  13422  xpscfn  13423  xpsc0  13424  xpsc1  13425  xpsfrnel  13427  xpsfrnel2  13429  xpsle  13445  ismred2  13467  acsfn  13523  0cat  13552  setcepi  13882  0pos  14050  meet0  14203  join0  14204  gsum0  14419  ga0  14714  oppglsm  14915  efgi0  14991  vrgpf  15039  vrgpinv  15040  frgpuptinv  15042  frgpup2  15047  0frgp  15050  frgpnabllem1  15123  frgpnabllem2  15124  dprd0  15228  dmdprdpr  15246  dprdpr  15247  00lsp  15700  fvcoe1  16250  coe1f2  16252  coe1sfi  16255  coe1add  16303  coe1mul2lem1  16306  coe1mul2lem2  16307  coe1mul2  16308  ply1coe  16330  frgpcyg  16489  topgele  16634  en1top  16684  en2top  16685  sn0topon  16697  indistopon  16700  indistps  16710  indistps2  16711  sn0cld  16789  indiscld  16790  rest0  16862  restsn  16863  cmpfi  17097  txindislem  17289  hmphindis  17450  xpstopnlem1  17462  xpstopnlem2  17464  ptcmpfi  17466  snfil  17521  fbasfip  17525  fgcl  17535  filcon  17540  fbasrn  17541  filuni  17542  cfinfil  17550  csdfil  17551  supfil  17552  ufildr  17588  fin1aufil  17589  rnelfmlem  17609  fclsval  17665  tmdgsum  17740  tsmsfbas  17772  0met  17892  xpsdsval  17907  minveclem3b  18754  evl1rhm  19374  evl1sca  19375  evl1var  19377  pf1mpf  19397  pf1ind  19400  tdeglem2  19409  deg1ldg  19440  deg1leb  19443  deg1val  19444  ulm0  19732  derang0  23072  indispcon  23137  umgra0  23249  vdgr0  23264  rdgprc  23520  dfrdg3  23522  trpredpred  23600  trpred0  23608  nosgnn0  23680  axdense  23712  fullfunfnv  23859  fullfunfv  23860  rank0  24175  ssoninhaus  24262  onint1  24263  alexeqd  24328  vxveqv  24420  ac5g  24441  snelpwg  24457  ab2rexexg  24489  fprg  24500  empos  24609  fisub  24921  0alg  25123  0ded  25124  0catOLD  25125  selsubf3g  25359  isconc1  25373  isconc2  25374  heibor1lem  25900  heiborlem6  25907  reheibor  25930  prter2  26116  mzpcompact2lem  26196  wopprc  26490  pw2f1ocnv  26497  pwslnmlem0  26560  fnchoice  27068  bnj941  27853  bnj97  27947  bnj149  27956  bnj150  27957  bnj944  28019
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2239  ax-nul 4123
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-ne 2423  df-v 2765  df-dif 3130  df-nul 3431
  Copyright terms: Public domain W3C validator