Theorem 0ex 1745

Description: The Null Set axiom of ZF set theory: the empty set exists. Corollary 5.16 of [TakeutiZaring] p. 20. In some textbooks this is presented as a separate axiom; here we show it can be derived from the Extensionality and Replacement axioms. It cannot be derived from these unless our predicate calculus includes an axiom stating that at least one set exists (which it does in the form of ax-9 799). For another version, see zfnul 1746.

Assertion

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

Proof of Theorem 0ex

Step	Hyp	Ref	Expression
1		in0 1722	. 2 |- (x i^i (/)) = (/)
2		visset 1350	. . 3 |- x e. V
3	2	inex1 1697	. 2 |- (x i^i (/)) e. V
4	1, 3	eqeltrr 1160	1 |- (/) e. V

Syntax hints:   e. wcel 1092  Vcvv 1348   i^i cin 1486  (/)c0 1707

This theorem is referenced by:  class2set 1747  snex 1859  pwpw0 1883  0nep0 1887  dtru 1889  zfpair 1891  opprc1b 1906  opprc3 1908  opthwiener 1914  uni0 1938  unidif0 1944  onint0 2262  0elon 2277  nsuceq0 2306  onzsl 2367  snsn0non 2371  finds 2397  finds2 2399  tfinds2 2405  opthprc 2457  fun0 2691  nfunv 2693  tz7.44-1 2966  el1o 3115  om0 3125  om0x 3126  map0e 3266  map0b 3267  en0 3328  ensn1 3329  en1 3331  2dom 3332  map1 3335  endisj 3341  pw2en 3348  0dom 3366  dom0 3367  0sdom 3368  limensuci 3401  nneneq 3408  inf3lemb 3461  inf5 3472  dfom3 3477  r10 3495  scottex 3541  cardeq0 3639  unxpdom2 3651  sucxpdom 3652  cf0 3705  cfsuc 3709  uncdadom 3718  cdaen 3719  cda0en 3720  cda1en 3721  xp1en 3722  cdacomen 3724  cdaassen 3725  cdadom1 3727  axpowndlem3 3745  elni 3798  1lt2pi 3826  indpi 3828

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-v 1349  df-dif 1489  df-in 1491  df-nul 1708

metamath.org