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

Theorem 0ex 4090
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 4089. (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 4089 . . 3  |-  E. x A. y  -.  y  e.  x
2 eq0 3411 . . . 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 2747 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 2740   (/)c0 3397
This theorem is referenced by:  class2set  4116  0elpw  4118  0nep0  4119  unidif0  4121  iin0  4122  notzfaus  4123  intv  4124  snexALT  4134  p0ex  4135  dtruALT  4145  zfpair  4150  snex  4154  dtruALT2  4157  opex  4174  opthwiener  4205  0elon  4382  nsuceq0  4409  snsn0non  4448  unisn2  4459  onint0  4524  tfinds2  4591  finds  4619  finds2  4621  opthprc  4689  xpexr  5067  soex  5075  dmsnsnsn  5103  nfunv  5189  fun0  5210  fvrn0  5449  fvssunirn  5450  brtpos0  6140  reldmtpos  6141  iotaex  6207  tfrlem16  6342  tz7.44-1  6352  seqomlem1  6395  1n0  6427  el1o  6431  om0  6449  map0e  6738  ixpexg  6773  0elixp  6780  en0  6857  ensn1  6858  en1  6861  2dom  6866  map1  6872  xp1en  6881  endisj  6882  pw2eng  6901  map2xp  6964  limensuci  6970  1sdom  6998  unxpdom2  7004  sucxpdom  7005  isinf  7009  ac6sfi  7034  fodomfi  7068  fi0  7106  oiexg  7183  brwdom  7214  brwdom2  7220  inf3lemb  7259  infeq5i  7270  dfom3  7281  cantnfvalf  7299  cantnfval2  7303  cantnflt  7306  cantnff  7308  cantnf0  7309  cantnfp1lem3  7315  cantnflem1d  7323  cantnflem1  7324  cantnf  7328  cnfcom  7336  tc0  7365  r10  7373  scottex  7488  infxpenlem  7574  fseqenlem1  7584  dfac9  7695  uncdadom  7730  cdaun  7731  cdaen  7732  cda1dif  7735  pm110.643  7736  cda0en  7738  cdacomen  7740  cdaassen  7741  xpcdaen  7742  mapcdaen  7743  cdaxpdom  7748  cdainf  7751  infcda1  7752  pwsdompw  7763  pwcdadom  7775  ackbij1lem14  7792  ackbij2lem2  7799  ackbij2lem3  7800  cf0  7810  cfeq0  7815  cfsuc  7816  cflim2  7822  isfin5  7858  isfin4-3  7874  fin1a2lem11  7969  fin1a2lem12  7970  fin1a2lem13  7971  axcc2lem  7995  ac6num  8039  zornn0g  8065  ttukeylem3  8071  brdom3  8086  iundom2g  8095  cardeq0  8107  alephadd  8132  pwcfsdom  8138  axpowndlem3  8154  canthwe  8206  canthp1lem1  8207  pwxpndom2  8220  pwcdandom  8222  gchxpidm  8224  intwun  8290  0tsk  8310  grothomex  8384  indpi  8464  fzennn  10961  hash0  11286  hashmap  11317  hashbc  11321  hashf1  11325  swrdval  11380  swrd00  11381  rexpen  12433  sadcf  12571  sadc0  12572  sadcp1  12573  smupf  12596  smup0  12597  smupp1  12598  0ram  12994  ram0  12996  str0  13111  ressbas  13125  ress0  13129  0rest  13261  xpscg  13387  xpscfn  13388  xpsc0  13389  xpsc1  13390  xpsfrnel  13392  xpsfrnel2  13394  xpsle  13410  ismred2  13432  acsfn  13488  0cat  13517  setcepi  13847  0pos  14015  meet0  14168  join0  14169  gsum0  14384  ga0  14679  oppglsm  14880  efgi0  14956  vrgpf  15004  vrgpinv  15005  frgpuptinv  15007  frgpup2  15012  0frgp  15015  frgpnabllem1  15088  frgpnabllem2  15089  dprd0  15193  dmdprdpr  15211  dprdpr  15212  00lsp  15665  fvcoe1  16215  coe1f2  16217  coe1sfi  16220  coe1add  16268  coe1mul2lem1  16271  coe1mul2lem2  16272  coe1mul2  16273  ply1coe  16295  frgpcyg  16454  topgele  16599  en1top  16649  en2top  16650  sn0topon  16662  indistopon  16665  indistps  16675  indistps2  16676  sn0cld  16754  indiscld  16755  rest0  16827  restsn  16828  cmpfi  17062  txindislem  17254  hmphindis  17415  xpstopnlem1  17427  xpstopnlem2  17429  ptcmpfi  17431  snfil  17486  fbasfip  17490  fgcl  17500  filcon  17505  fbasrn  17506  filuni  17507  cfinfil  17515  csdfil  17516  supfil  17517  ufildr  17553  fin1aufil  17554  rnelfmlem  17574  fclsval  17630  tmdgsum  17705  tsmsfbas  17737  0met  17857  xpsdsval  17872  minveclem3b  18719  evl1rhm  19339  evl1sca  19340  evl1var  19342  pf1mpf  19362  pf1ind  19365  tdeglem2  19374  deg1ldg  19405  deg1leb  19408  deg1val  19409  ulm0  19697  derang0  23037  indispcon  23102  umgra0  23214  vdgr0  23229  rdgprc  23485  dfrdg3  23487  trpredpred  23565  trpred0  23573  nosgnn0  23645  axdense  23677  fullfunfnv  23824  fullfunfv  23825  rank0  24140  ssoninhaus  24227  onint1  24228  alexeqd  24293  vxveqv  24385  ac5g  24406  snelpwg  24422  ab2rexexg  24454  fprg  24465  empos  24574  fisub  24886  0alg  25088  0ded  25089  0catOLD  25090  selsubf3g  25324  isconc1  25338  isconc2  25339  heibor1lem  25865  heiborlem6  25872  reheibor  25895  prter2  26081  mzpcompact2lem  26161  wopprc  26455  pw2f1ocnv  26462  pwslnmlem0  26525  fnchoice  27033  bnj941  27816  bnj97  27910  bnj149  27919  bnj150  27920  bnj944  27982
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 2237  ax-nul 4089
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 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-ne 2421  df-v 2742  df-dif 3097  df-nul 3398
  Copyright terms: Public domain W3C validator