Theorem 0ex 2717

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

Assertion

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

Proof of Theorem 0ex

Step	Hyp	Ref	Expression
1		ax-nul 2716	. . . 4 |- E.xA.y -. y e. x
2	1	zfnuleu 2713	. . 3 |- E!xA.y -. y e. x
3		eq0 2299	. . . 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 2284

This theorem is referenced by:  class2set 2740  0elpw 2742  0nep0 2743  unidif0 2745  iin0 2746  notzfaus 2747  intv 2748  dtru 2779  zfpair 2784  opprc1b 2803  opprc3 2804  opthwiener 2814  unisn2 2882  onint0 3014  0elon 3029  nsuceq0 3060  onzsl 3124  snsn0non 3132  finds 3163  finds2 3165  tfinds2 3172  opthprc 3228  onnev 3249  xpexr 3486  fun0 3551  nfunv 3553  tz7.44-1 3935  1ne0 4149  el1o 4153  om0 4163  om0x 4165  map0e 4349  map0b 4350  map0 4351  0elixp 4367  en0 4430  ensn1 4431  en1 4433  2dom 4434  map1 4437  endisj 4444  pw2en 4453  0dom 4471  dom0 4472  0sdomg 4473  limensuci 4513  unifiOLD 4574  inf3lemb 4626  infeq5 4637  dfom3 4646  r10 4668  scottex 4733  brdom3 4818  cardeq0 4849  unxpdom2 4863  sucxpdom 4864  cf0 4929  cfeq0 4933  cfsuc 4934  uncdadom 4940  cdaun 4941  pm110.643 4942  cdaen 4943  cda0en 4944  cda1en 4945  xp1en 4946  cdacomen 4948  cdaassen 4949  mapcdaen 4951  cdadom1 4952  axpowndlem3 4970  indpi 5053  acdc3lem 7494  acdc2lem1 7496  acdclem 7502  alephadd 7591  sn0top 7651  indistop 7652  indistps 7657  0met 7829  bcth 8036  moec 10459  intprd 10469  vxveqv 10475  mapudiscn 10506  eqindhome 10535  top1 10541  top2ind 10542  top2usne 10543  homindlem2 10544  homindlem3 10545  efilcp 10564  fisub 10566  efilcp2 10569  cnfilca 10570  rcfpfillem2 10572  rcfpfillem3 10573  rcfpfillem5 10575  0alg 10668  0ded 10669  0cat 10670  hgrablkcard 10753  emhgrat 10754  0hgra 10755

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 2716

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 2053  df-nul 2285

Copyright terms: Public domain