Theorem uni0 4278

Description: The union of the empty set is the empty set. Theorem 8.7 of [Quine] p. 54. (Reproved without relying on ax-nul 4586 by Eric Schmidt.) (Contributed by NM, 16-Sep-1993.) (Revised by Eric Schmidt, 4-Apr-2007.)

Assertion

Ref	Expression
uni0	|- U. (/) = (/)

Proof of Theorem uni0

Step	Hyp	Ref	Expression
1		0ss 3823	. 2 |- (/) C_ { (/) }
2		uni0b 4276	. 2 |- ( U. (/) = (/) <-> (/) C_ { (/) } )
3	1, 2	mpbir 209	1 |- U. (/) = (/)

Syntax hints:   = wceq 1395   C_ wss 3471   (/)c0 3793   {csn 4032   U.cuni 4251

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-v 3111  df-dif 3474  df-in 3478  df-ss 3485  df-nul 3794  df-sn 4033  df-uni 4252

This theorem is referenced by:  csbuni  4279  uniintsn  4326  iununi  4420  unisn2  4592  unizlim  5003  opswap  5501  unixp0  5547  unixpid  5548  iotanul  5572  funfv  5940  dffv2  5946  1stval  6801  2ndval  6802  1stnpr  6803  2ndnpr  6804  1st0  6805  2nd0  6806  1st2val  6825  2nd2val  6826  brtpos0  6980  tpostpos  6993  nnunifi  7789  supval2  7932  infeq5  8071  rankuni  8298  rankxplim3  8316  iunfictbso  8512  cflim2  8660  fin1a2lem11  8807  itunisuc  8816  itunitc  8818  ttukeylem4  8909  incexclem  13660  arwval  15449  dprdsn  17210  zrhval  18672  0opn  19540  indistopon  19629  mretopd  19720  hauscmplem  20033  cmpfi  20035  comppfsc  20159  alexsublem  20670  alexsubALTlem2  20674  ptcmplem2  20679  lebnumlem3  21589  locfinref  28005  prsiga  28304  dya2iocuni  28427  fiunelcarsg  28459  carsgclctunlem1  28460  carsgclctunlem3  28462  unisnif  29780  limsucncmpi  30115  heicant  30254  ovoliunnfl  30261  voliunnfl  30263  volsupnfl  30264  mbfresfi  30266  stoweidlem35  32020  stoweidlem39  32024