Theorem uni0 4139

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

Syntax hints:   = wceq 1369   C_ wss 3349   (/)c0 3658   {csn 3898   U.cuni 4112

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-ral 2741  df-rex 2742  df-v 2995  df-dif 3352  df-in 3356  df-ss 3363  df-nul 3659  df-sn 3899  df-uni 4113

This theorem is referenced by:  csbuni  4140  uniintsn  4186  iununi  4276  unisn2  4449  unizlim  4856  opswap  5347  unixp0  5392  unixpid  5393  iotanul  5417  funfv  5779  dffv2  5785  1stval  6600  2ndval  6601  1stnpr  6602  2ndnpr  6603  1st0  6604  2nd0  6605  1st2val  6623  2nd2val  6624  brtpos0  6773  tpostpos  6786  nnunifi  7584  supval2  7726  infeq5  7864  rankuni  8091  rankxplim3  8109  iunfictbso  8305  cflim2  8453  fin1a2lem11  8600  itunisuc  8609  itunitc  8611  ttukeylem4  8702  incexclem  13320  arwval  14932  dprdsn  16555  zrhval  17961  0opn  18539  indistopon  18627  mretopd  18718  hauscmplem  19031  cmpfi  19033  alexsublem  19638  alexsubALTlem2  19642  ptcmplem2  19647  lebnumlem3  20557  prsiga  26596  dya2iocuni  26720  unisnif  27978  limsucncmpi  28313  heicant  28452  ovoliunnfl  28459  voliunnfl  28461  volsupnfl  28462  mbfresfi  28464  comppfsc  28605  stoweidlem35  29856  stoweidlem39  29860