Theorem 0ex 3614

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 3613. (The proof was shortened by Andrew Salmon, 9-Jul-2011.)

Assertion

Ref	Expression
0ex	|- (/) e. _V

Proof of Theorem 0ex

Step	Hyp	Ref	Expression
1		ax-nul 3613	. . 3 |- E.xA.y -. y e. x
2		eq0 3096	. . . 4 |- (x = (/) <-> A.y -. y e. x)
3	2	exbii 1687	. . 3 |- (E.x x = (/) <-> E.xA.y -. y e. x)
4	1, 3	mpbir 273	. 2 |- E.x x = (/)
5		isset 2542	. 2 |- ((/) e. _V <-> E.x x = (/))
6	4, 5	mpbir 273	1 |- (/) e. _V

Syntax hints:  -. wn 2  A.wal 1584   = wceq 1586   e. wcel 1588  E.wex 1615  _Vcvv 2538  (/)c0 3082

This theorem is referenced by:  class2set 3639  0elpw 3641  0nep0 3642  unidif0 3644  iin0 3645  notzfaus 3646  intv 3647  snex 3657  dtruALT 3680  zfpair 3685  opprc1b 3705  opprc3 3706  opthwiener 3717  0elon 3863  nsuceq0 3891  snsn0non 3928  unisn2 3938  onint0 4020  tfinds2 4083  finds 4112  finds2 4114  opthprc 4179  onnevOLD 4203  xpexr 4458  nfunv 4555  fun0 4573  iotaex 5233  tz7.44-1 5300  1n0 5353  el1o 5357  om0 5367  om0x 5369  map0e 5562  map0b 5563  map0 5564  0elixp 5580  en0 5643  ensn1 5644  en1 5646  2dom 5647  fndmeng 5649  mapsnen 5650  map1 5652  endisj 5660  pw2en 5671  ac6sfi 5675  0dom 5693  dom0 5694  0sdomg 5695  xpnum 5771  limensuci 5791  1sdom 5815  unxpdom2 5821  sucxpdom 5822  isinf 5828  card2inf 5927  inf3lemb 5948  infeq5 5960  dfom3 5972  r10 5998  scottex 6085  cardval3 6104  dif1cardOLD 6144  infxpenlem 6147  omsublim 6178  onssnum 6207  uncdadom 6239  cdaun 6240  cda1en 6241  pm110.643 6243  cdaen 6244  cda0en 6246  xp1en 6247  cdacomen 6249  cdaassen 6250  mapcdaen 6252  cdadom1 6253  cdainf 6258  pwsdompw 6264  cf0 6270  cfeq0 6275  cfsuc 6276  cflim2 6283  axcc2lem 6293  ac6sgOLD 6331  brdom3 6377  cardeq0 6396  cfeq0OLD 6446  cfsucOLD 6447  pwcfsdom 6450  cda1enOLD 6453  axpowndlem3 6469  indpi 6552  fzennn 8090  acdc3lem 9152  acdc2lem1 9155  acdclem 9161  alephadd 9245  sn0top 9768  indistop 9769  indistpsOLD 9774  indistpsx 9776  indistps 9777  indistps2 9778  0met 9968  bcth 10176  gid0 10207  grpoidval 10211  ga0 10322  vacnlem4 10539  vacnlem5 10540  subsp 11080  issubsplem1 11082  fsubbas 11119  fbunfip 11120  filrn 11131  bnj147 13260  bnj148 13261  bnj519 13293  bnj941 13613  bnj97 13991  bnj102 13993  bnj149 14012  bnj583 14067  bnj894 14098  bnj939 14109  fvrn0 14468  trpredpred 14580  trpred0 14588  sltval2 14662  nosgnn0 14664  sltsgn1 14667  sltsgn2 14668  sltintdifex 14669  sltres 14670  axsltsolem1 14674  axdenselem8 14695  axdense 14696  axfelem9 14707  axfelem10 14708  alexeqd 15002  moec 15059  vxveqv 15067  ac5g 15098  snelpwg 15127  pw2eng 15131  prnzgOLD 15166  ab2rexexg 15183  empos 15322  topindisOLD 15612  topindis 15613  mapudiscn 15629  distopg 15633  eqindhome 15652  top1 15653  top2ind 15654  top2usne 15655  homindlem2 15656  homindlem3 15657  subsp2OLD 15664  subspemp 15665  sbtpsines 15667  prtoptop 15684  efilcp 15688  fisub 15690  efilcp2 15692  cnfilca 15693  rcfpfillem2 15695  rcfpfillem3 15696  rcfpfillem5 15698  limfillem2 15705  clsingemp 15739  clindistop 15740  clindistop2 15741  intopcon 15742  singempcon 15743  topsinind 15745  extopgrp 15758  topgrpsubcn 15760  0alg 15897  0ded 15898  0cat 15899  empistar 16029  omsublimOLD 16220  compfipin0 16260  topmtcl 16349  topjoin 16351  fbasfip 16380  supfil 16384  ufinffr 16402  ufilen 16403  filcon 16404  ufcondr 16405  rnelfmlem 16416  erthdmg 16554  zornn0 16588  iserzshft2 16653  isumshft2 16654  heiborlem13 16791  heiborlem18 16796  heiborlem42 16820  prter2 17109  hgrablkcard 17120  emhgrat 17121  0hgra 17122

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1592  ax-gen 1593  ax-8 1594  ax-9 1595  ax-10 1596  ax-11 1597  ax-12 1598  ax-17 1605  ax-4 1608  ax-5o 1610  ax-6o 1613  ax-9o 1763  ax-10o 1781  ax-16 1854  ax-11o 1864  ax-ext 2123  ax-nul 3613

This theorem depends on definitions:  df-bi 220  df-or 338  df-an 339  df-ex 1616  df-sb 1816  df-clab 2129  df-cleq 2134  df-clel 2137  df-ne 2268  df-v 2540  df-dif 2830  df-nul 3083

Copyright terms: Public domain