Theorem 0ex 2701

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

Assertion

Ref	Expression
0ex	⊢ ∅ ∈ V

Proof of Theorem 0ex

Step	Hyp	Ref	Expression
1		ax-nul 2700	. . . 4 ⊢ ∃x∀y ¬ y ∈ x
2	1	zfnuleu 2697	. . 3 ⊢ ∃!x∀y ¬ y ∈ x
3		eq0 2284	. . . 4 ⊢ (x = ∅ ↔ ∀y ¬ y ∈ x)
4	3	eubii 1380	. . 3 ⊢ (∃!x x = ∅ ↔ ∃!x∀y ¬ y ∈ x)
5	2, 4	mpbir 190	. 2 ⊢ ∃!x x = ∅
6		eueq 1907	. 2 ⊢ (∅ ∈ V ↔ ∃!x x = ∅)
7	5, 6	mpbir 190	1 ⊢ ∅ ∈ V

Syntax hints:  ¬ wn 2  ∀wal 951   = wceq 953   ∈ wcel 955  ∃!weu 1373  Vcvv 1802  ∅c0 2270

This theorem is referenced by:  class2set 2724  0elpw 2726  0nep0 2727  unidif0 2729  iin0 2730  notzfaus 2731  dtru 2762  zfpair 2767  opprc1b 2786  opprc3 2787  opthwiener 2796  unisn2 2866  onint0 2997  0elon 3012  nsuceq0 3043  onzsl 3107  snsn0non 3115  finds 3146  finds2 3148  tfinds2 3155  opthprc 3211  onnev 3232  xpexr 3465  fun0 3530  nfunv 3532  tz7.44-1 3913  1ne0 4126  el1o 4130  om0 4140  om0x 4142  map0e 4326  map0b 4327  map0 4328  0elixp 4344  en0 4404  ensn1 4405  en1 4407  2dom 4408  map1 4411  endisj 4417  pw2en 4426  0dom 4444  dom0 4445  0sdomg 4446  limensuci 4486  unifi 4532  inf3lemb 4582  infeq5 4593  dfom3 4602  r10 4623  scottex 4688  brdom3 4773  cardeq0 4804  unxpdom2 4817  sucxpdom 4818  cf0 4882  cfeq0 4886  cfsuc 4887  uncdadom 4893  cdaun 4894  pm110.643 4895  cdaen 4896  cda0en 4897  cda1en 4898  xp1en 4899  cdacomen 4901  cdaassen 4902  mapcdaen 4904  cdadom1 4905  axpowndlem3 4923  indpi 5006  acdc3lem 7428  acdc2lem1 7430  acdclem 7436  alephadd 7524  sn0top 7589  indistop 7590  indistps 7595  0met 7765  bcth 7966  moec 10357  intprd 10367  mapudiscn 10399  efilcp 10445  fisub 10447  efilcp2 10450  cnfilca 10451  relrded 10519  0alg 10533  0ded 10534  0cat 10535  relrcat 10540  hgrablkcard 10610  emhgrat 10611  0hgra 10612

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-11 964  ax-12 965  ax-14 967  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452  ax-nul 2700

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 978  df-sb 1168  df-eu 1375  df-mo 1376  df-clab 1457  df-cleq 1462  df-clel 1465  df-ne 1579  df-v 1803  df-dif 2039  df-nul 2271

Copyright terms: Public domain