Theorem 0ex 2679

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

Assertion

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

Proof of Theorem 0ex

Step	Hyp	Ref	Expression
1		ax-nul 2678	. . . 4 |- E.xA.y -. y e. x
2	1	zfnuleu 2675	. . 3 |- E!xA.y -. y e. x
3		eq0 2265	. . . 4 |- (x = (/) <-> A.y -. y e. x)
4	3	eubii 1364	. . 3 |- (E!x x = (/) <-> E!xA.y -. y e. x)
5	2, 4	mpbir 190	. 2 |- E!x x = (/)
6		eueq 1888	. 2 |- ((/) e. V <-> E!x x = (/))
7	5, 6	mpbir 190	1 |- (/) e. V

Syntax hints:  -. wn 2  A.wal 950   = wceq 1099   e. wcel 1105  E!weu 1357  Vcvv 1786  (/)c0 2251

This theorem is referenced by:  class2set 2702  0elpw 2704  0nep0 2705  unidif0 2707  iin0 2708  notzfaus 2709  dtru 2740  zfpair 2745  opprc1b 2763  opprc3 2764  opthwiener 2770  unisn2 2839  onint0 2970  0elon 2985  nsuceq0 3016  onzsl 3080  snsn0non 3088  finds 3119  finds2 3121  tfinds2 3128  opthprc 3183  onnev 3204  xpexr 3425  fun0 3485  nfunv 3487  tz7.44-1 3867  1ne0 4080  el1o 4084  om0 4094  om0x 4096  map0e 4280  map0b 4281  map0 4282  0elixp 4298  en0 4358  ensn1 4359  en1 4361  2dom 4362  map1 4365  endisj 4371  pw2en 4380  0dom 4398  dom0 4399  0sdomg 4400  limensuci 4438  unifi 4484  inf3lemb 4534  infeq5 4545  dfom3 4554  r10 4575  scottex 4640  brdom3 4725  cardeq0 4756  unxpdom2 4768  sucxpdom 4769  cf0 4833  cfeq0 4837  cfsuc 4838  uncdadom 4844  cdaun 4845  pm110.643 4846  cdaen 4847  cda0en 4848  cda1en 4849  xp1en 4850  cdacomen 4852  cdaassen 4853  mapcdaen 4855  cdadom1 4856  axpowndlem3 4874  indpi 4957  acdc3lem 7379  acdc2lem1 7381  acdclem 7387  alephadd 7475  sn0top 7540  indistop 7541  indistps 7546  0met 7713  bcth 7914  symggrp 8675  moec 8716  intprd 8726  efilcp 8795  fisub 8797  efilcp2 8800  cnfilca 8801  relrded 8869  0alg 8883  0ded 8884  0cat 8885  relrcat 8890  hgrablkcard 8956  emhgrat 8957  0hgra 8958

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-6 953  ax-7 954  ax-gen 955  ax-8 1101  ax-9 1102  ax-10 1103  ax-12 1104  ax-14 1108  ax-11 1180  ax-17 1190  ax-16 1194  ax-11o 1202  ax-ext 1436  ax-nul 2678

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 957  df-sb 1155  df-eu 1359  df-mo 1360  df-clab 1441  df-cleq 1446  df-clel 1449  df-ne 1563  df-v 1787  df-dif 2020  df-nul 2252

Copyright terms: Public domain