Theorem 0ex 2711

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 2710.

Assertion

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

Proof of Theorem 0ex

Step	Hyp	Ref	Expression
1		ax-nul 2710	. . . 4 |- E.xA.y -. y e. x
2	1	zfnuleu 2707	. . 3 |- E!xA.y -. y e. x
3		eq0 2294	. . . 4 |- (x = (/) <-> A.y -. y e. x)
4	3	eubii 1387	. . 3 |- (E!x x = (/) <-> E!xA.y -. y e. x)
5	2, 4	mpbir 190	. 2 |- E!x x = (/)
6		eueq 1916	. 2 |- ((/) e. V <-> E!x x = (/))
7	5, 6	mpbir 190	1 |- (/) e. V

Syntax hints:  -. wn 2  A.wal 954   = wceq 956   e. wcel 958  E!weu 1380  Vcvv 1811  (/)c0 2280

This theorem is referenced by:  class2set 2734  0elpw 2736  0nep0 2737  unidif0 2739  iin0 2740  notzfaus 2741  dtru 2772  zfpair 2777  opprc1b 2796  opprc3 2797  opthwiener 2807  unisn2 2875  onint0 3007  0elon 3022  nsuceq0 3053  onzsl 3117  snsn0non 3125  finds 3156  finds2 3158  tfinds2 3165  opthprc 3221  onnev 3242  xpexr 3479  fun0 3544  nfunv 3546  tz7.44-1 3928  1ne0 4142  el1o 4146  om0 4156  om0x 4158  map0e 4342  map0b 4343  map0 4344  0elixp 4360  en0 4423  ensn1 4424  en1 4426  2dom 4427  map1 4430  endisj 4437  pw2en 4446  0dom 4464  dom0 4465  0sdomg 4466  limensuci 4506  unifiOLD 4557  inf3lemb 4610  infeq5 4621  dfom3 4630  r10 4651  scottex 4716  brdom3 4801  cardeq0 4832  unxpdom2 4845  sucxpdom 4846  cf0 4910  cfeq0 4914  cfsuc 4915  uncdadom 4921  cdaun 4922  pm110.643 4923  cdaen 4924  cda0en 4925  cda1en 4926  xp1en 4927  cdacomen 4929  cdaassen 4930  mapcdaen 4932  cdadom1 4933  axpowndlem3 4951  indpi 5034  acdc3lem 7486  acdc2lem1 7488  acdclem 7494  alephadd 7582  sn0top 7647  indistop 7648  indistps 7653  0met 7825  bcth 8032  moec 10461  intprd 10471  mapudiscn 10512  eqindhome 10541  top1 10547  top2ind 10548  top2usne 10549  homindlem2 10550  homindlem3 10551  efilcp 10572  efilcpOLD 10573  fisub 10576  fisubOLD 10577  efilcp2 10581  efilcp2OLD 10582  cnfilca 10583  cnfilcaOLD 10584  rcfpfillem2 10587  rcfpfillem2OLD 10588  rcfpfillem3 10589  rcfpfillem3OLD 10590  rcfpfillem5 10593  rcfpfillem5OLD 10594  relrded 10675  0alg 10689  0ded 10690  0cat 10691  relrcat 10696  hgrablkcard 10774  emhgrat 10775  0hgra 10776

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-11 967  ax-12 968  ax-14 970  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459  ax-nul 2710

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 981  df-sb 1172  df-eu 1382  df-mo 1383  df-clab 1464  df-cleq 1469  df-clel 1472  df-ne 1587  df-v 1812  df-dif 2049  df-nul 2281

Copyright terms: Public domain