Theorem uni0 4106

Description: The union of the empty set is the empty set. Theorem 8.7 of [Quine] p. 54. (Reproved without relying on ax-nul 4409 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 3654	. 2 |- (/) C_ { (/) }
2		uni0b 4104	. 2 |- ( U. (/) = (/) <-> (/) C_ { (/) } )
3	1, 2	mpbir 209	1 |- U. (/) = (/)

Syntax hints:   = wceq 1362   C_ wss 3316   (/)c0 3625   {csn 3865   U.cuni 4079

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-v 2964  df-dif 3319  df-in 3323  df-ss 3330  df-nul 3626  df-sn 3866  df-uni 4080

This theorem is referenced by:  csbuni  4107  uniintsn  4153  iununi  4243  unisn2  4416  unizlim  4822  opswap  5314  unixp0  5359  unixpid  5360  iotanul  5384  funfv  5746  dffv2  5752  1stval  6568  2ndval  6569  1stnpr  6570  2ndnpr  6571  1st0  6572  2nd0  6573  1st2val  6591  2nd2val  6592  brtpos0  6741  tpostpos  6754  nnunifi  7551  supval2  7693  infeq5  7831  rankuni  8058  rankxplim3  8076  iunfictbso  8272  cflim2  8420  fin1a2lem11  8567  itunisuc  8576  itunitc  8578  ttukeylem4  8669  incexclem  13281  arwval  14893  dprdsn  16506  zrhval  17780  0opn  18358  indistopon  18446  mretopd  18537  hauscmplem  18850  cmpfi  18852  alexsublem  19457  alexsubALTlem2  19461  ptcmplem2  19466  lebnumlem3  20376  prsiga  26427  dya2iocuni  26551  unisnif  27802  limsucncmpi  28138  heicant  28267  ovoliunnfl  28274  voliunnfl  28276  volsupnfl  28277  mbfresfi  28279  comppfsc  28420  stoweidlem35  29673  stoweidlem39  29677