Theorem 0ex 2716

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

Assertion

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

Proof of Theorem 0ex

Step	Hyp	Ref	Expression
1		ax-nul 2715	. . . 4 |- E.xA.y -. y e. x
2	1	zfnuleu 2712	. . 3 |- E!xA.y -. y e. x
3		eq0 2298	. . . 4 |- (x = (/) <-> A.y -. y e. x)
4	3	eubii 1389	. . 3 |- (E!x x = (/) <-> E!xA.y -. y e. x)
5	2, 4	mpbir 190	. 2 |- E!x x = (/)
6		eueq 1919	. 2 |- ((/) e. V <-> E!x x = (/))
7	5, 6	mpbir 190	1 |- (/) e. V

Syntax hints:  -. wn 2  A.wal 956   = wceq 958   e. wcel 960  E!weu 1382  Vcvv 1814  (/)c0 2283

This theorem is referenced by:  class2set 2739  0elpw 2741  0nep0 2742  unidif0 2744  iin0 2745  notzfaus 2746  intv 2747  dtru 2778  zfpair 2783  opprc1b 2802  opprc3 2803  opthwiener 2813  unisn2 2881  onint0 3013  0elon 3028  nsuceq0 3059  onzsl 3123  snsn0non 3131  finds 3162  finds2 3164  tfinds2 3171  opthprc 3227  onnev 3248  xpexr 3485  fun0 3550  nfunv 3552  tz7.44-1 3934  1ne0 4148  el1o 4152  om0 4162  om0x 4164  map0e 4348  map0b 4349  map0 4350  0elixp 4366  en0 4429  ensn1 4430  en1 4432  2dom 4433  map1 4436  endisj 4443  pw2en 4452  0dom 4470  dom0 4471  0sdomg 4472  limensuci 4512  unifiOLD 4570  inf3lemb 4619  infeq5 4630  dfom3 4639  r10 4661  scottex 4726  brdom3 4811  cardeq0 4842  unxpdom2 4856  sucxpdom 4857  cf0 4922  cfeq0 4926  cfsuc 4927  uncdadom 4933  cdaun 4934  pm110.643 4935  cdaen 4936  cda0en 4937  cda1en 4938  xp1en 4939  cdacomen 4941  cdaassen 4942  mapcdaen 4944  cdadom1 4945  axpowndlem3 4963  indpi 5046  acdc3lem 7487  acdc2lem1 7489  acdclem 7495  alephadd 7584  sn0top 7644  indistop 7645  indistps 7650  0met 7822  bcth 8029  moec 10451  intprd 10461  vxveqv 10467  mapudiscn 10498  eqindhome 10527  top1 10533  top2ind 10534  top2usne 10535  homindlem2 10536  homindlem3 10537  efilcp 10556  fisub 10558  efilcp2 10561  cnfilca 10562  rcfpfillem2 10564  rcfpfillem3 10565  rcfpfillem5 10567  0alg 10660  0ded 10661  0cat 10662  hgrablkcard 10745  emhgrat 10746  0hgra 10747

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-11 969  ax-12 970  ax-14 972  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462  ax-nul 2715

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 983  df-sb 1174  df-eu 1384  df-mo 1385  df-clab 1467  df-cleq 1472  df-clel 1475  df-ne 1590  df-v 1815  df-dif 2052  df-nul 2284

Copyright terms: Public domain