Theorem 0ex 3261

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 3260. (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 3260	. . 3 |- E.xA.y -. y e. x
2		eq0 2718	. . . 4 |- (x = (/) <-> A.y -. y e. x)
3	2	exbii 1236	. . 3 |- (E.x x = (/) <-> E.xA.y -. y e. x)
4	1, 3	mpbir 206	. 2 |- E.x x = (/)
5		isset 2129	. 2 |- ((/) e. _V <-> E.x x = (/))
6	4, 5	mpbir 206	1 |- (/) e. _V

Syntax hints:  -. wn 2  A.wal 1134   = wceq 1136   e. wcel 1138  E.wex 1164  _Vcvv 2125  (/)c0 2701

This theorem is referenced by:  class2set 3286  0elpw 3288  0nep0 3289  unidif0 3291  iin0 3292  notzfaus 3293  intv 3294  snex 3307  dtruALT 3332  zfpair 3337  opprc1b 3357  opprc3 3358  opthwiener 3369  0elon 3531  nsuceq0 3561  snsn0non 3599  snsn0nonOLD 3600  unisn2 3610  onint0 3688  onzslOLD 3740  tfinds2 3758  finds 3790  finds2 3792  opthprc 3857  onnev 3881  xpexr 4163  nfunv 4264  fun0 4283  iotaex 4910  tz7.44-1 4947  1n0 4998  el1o 5002  om0 5012  om0x 5014  map0e 5212  map0b 5213  map0 5214  0elixp 5230  en0 5293  ensn1 5294  en1 5296  2dom 5297  map1 5300  endisj 5307  pw2en 5316  ac6sfi 5320  0dom 5338  dom0 5339  0sdomg 5340  limensuci 5410  inf3lemb 5525  infeq5 5536  dfom3 5546  r10 5571  scottex 5642  omsublim 5683  brdom3 5759  cardeq0 5778  unxpdom2 5793  sucxpdom 5794  cf0 5854  cfeq0 5858  cfsuc 5859  uncdadom 5865  cdaun 5866  pm110.643 5868  cdaen 5869  cda0en 5871  cda1en 5872  xp1en 5873  cdacomen 5875  cdaassen 5876  mapcdaen 5878  cdadom1 5879  axpowndlem3 5899  indpi 5982  acdc3lem 8549  acdc2lem1 8552  acdclem 8558  alephadd 8646  sn0top 8712  indistop 8713  indistps 8718  0met 8897  bcth 9105  gid0 9133  grpidval 9137  ga0 9248  vacnlem4 9465  vacnlem5 9466  dif1card 9969  ac6sg 9981  issubsplem1 10038  fsubbas 10073  fbunfip 10074  filrn 10085  bnj147 12272  bnj148 12273  bnj209OLD 12293  bnj210OLD 12295  bnj211OLD 12297  bnj519 12312  bnj941 12634  bnj97 13012  bnj102 13014  bnj149 13033  bnj583 13088  bnj894 13119  bnj939 13130  fndmeng 13390  fvrn0 13630  trclpred 13726  sltval2 13789  nosgnn0 13791  sltsgn1 13794  sltsgn2 13795  axsltsolem1 13796  axdenselem8 13816  axdense 13817  axfelem8 13828  axfelem9 13829  moec 14079  vxveqv 14085  ac5g 14118  snelpwg 14145  pw2eng 14149  prnzg 14183  empos 14306  topindis 14582  mapudiscn 14593  distopg 14597  eqindhome 14615  top1 14616  top2ind 14617  top2usne 14618  homindlem2 14619  homindlem3 14620  subsp2 14621  subspemp 14622  sbtpsines 14624  efilcp 14636  fisub 14638  efilcp2 14640  cnfilca 14641  rcfpfillem2 14643  rcfpfillem3 14644  rcfpfillem5 14646  limfillem2 14653  clsingemp 14675  clindistop 14676  clindistop2 14677  intopcon 14678  singempcon 14679  topsinind 14681  extopgrp 14694  topgrpsubcn 14696  0alg 14785  0ded 14786  0cat 14787  empistar 14901  omsublimOLD 15078  compfipin0 15118  topmtcl 15207  topjoin 15209  fbasfip 15238  supfil 15242  ufinffr 15260  ufilen 15261  filcon 15262  ufcondr 15263  rnelfmlem 15274  erthdmg 15412  zornn0 15446  iserzshft2 15511  isumshft2 15512  heiborlem13 15649  heiborlem18 15654  heiborlem42 15678  prter2 15967  hgrablkcard 15978  emhgrat 15979  0hgra 15980

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1142  ax-gen 1143  ax-8 1144  ax-9 1145  ax-10 1146  ax-11 1147  ax-12 1148  ax-17 1155  ax-4 1157  ax-5o 1159  ax-6o 1162  ax-9o 1319  ax-10o 1338  ax-16 1418  ax-11o 1426  ax-ext 1702  ax-nul 3260

This theorem depends on definitions:  df-bi 163  df-or 240  df-an 241  df-ex 1165  df-sb 1374  df-clab 1709  df-cleq 1714  df-clel 1717  df-ne 1856  df-v 2127  df-dif 2430  df-nul 2702

Copyright terms: Public domain