Theorem 0ex 2707

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

Assertion

Ref	Expression
0ex	⊢ ∅ ∈ V

Proof of Theorem 0ex

Step	Hyp	Ref	Expression
1		ax-nul 2706	. . . 4 ⊢ ∃x∀y ¬ y ∈ x
2	1	zfnuleu 2703	. . 3 ⊢ ∃!x∀y ¬ y ∈ x
3		eq0 2290	. . . 4 ⊢ (x = ∅ ↔ ∀y ¬ y ∈ x)
4	3	eubii 1385	. . 3 ⊢ (∃!x x = ∅ ↔ ∃!x∀y ¬ y ∈ x)
5	2, 4	mpbir 190	. 2 ⊢ ∃!x x = ∅
6		eueq 1912	. 2 ⊢ (∅ ∈ V ↔ ∃!x x = ∅)
7	5, 6	mpbir 190	1 ⊢ ∅ ∈ V

Syntax hints:  ¬ wn 2  ∀wal 952   = wceq 954   ∈ wcel 956  ∃!weu 1378  Vcvv 1807  ∅c0 2276

This theorem is referenced by:  class2set 2730  0elpw 2732  0nep0 2733  unidif0 2735  iin0 2736  notzfaus 2737  dtru 2768  zfpair 2773  opprc1b 2792  opprc3 2793  opthwiener 2804  unisn2 2874  onint0 3007  0elon 3022  nsuceq0 3053  onzsl 3117  snsn0non 3125  finds 3156  finds2 3158  tfinds2 3165  opthprc 3221  onnev 3242  xpexr 3480  fun0 3546  nfunv 3548  tz7.44-1 3930  1ne0 4143  el1o 4147  om0 4157  om0x 4159  map0e 4343  map0b 4344  map0 4345  0elixp 4361  en0 4421  ensn1 4422  en1 4424  2dom 4425  map1 4428  endisj 4434  pw2en 4443  0dom 4461  dom0 4462  0sdomg 4463  limensuci 4504  unifi 4550  inf3lemb 4602  infeq5 4613  dfom3 4622  r10 4643  scottex 4708  brdom3 4793  cardeq0 4824  unxpdom2 4837  sucxpdom 4838  cf0 4902  cfeq0 4906  cfsuc 4907  uncdadom 4913  cdaun 4914  pm110.643 4915  cdaen 4916  cda0en 4917  cda1en 4918  xp1en 4919  cdacomen 4921  cdaassen 4922  mapcdaen 4924  cdadom1 4925  axpowndlem3 4943  indpi 5026  acdc3lem 7448  acdc2lem1 7450  acdclem 7456  alephadd 7544  sn0top 7609  indistop 7610  indistps 7615  0met 7789  bcth 7994  moec 10429  intprd 10439  mapudiscn 10471  efilcp 10517  fisub 10519  efilcp2 10522  cnfilca 10523  relrded 10591  0alg 10605  0ded 10606  0cat 10607  relrcat 10612  hgrablkcard 10682  emhgrat 10683  0hgra 10684

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-11 965  ax-12 966  ax-14 968  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457  ax-nul 2706

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979  df-sb 1170  df-eu 1380  df-mo 1381  df-clab 1462  df-cleq 1467  df-clel 1470  df-ne 1584  df-v 1808  df-dif 2045  df-nul 2277

Copyright terms: Public domain