Theorem uni0 4218

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

Syntax hints:   = wceq 1405   C_ wss 3414   (/)c0 3738   {csn 3972   U.cuni 4191

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-ral 2759  df-rex 2760  df-v 3061  df-dif 3417  df-in 3421  df-ss 3428  df-nul 3739  df-sn 3973  df-uni 4192

This theorem is referenced by:  csbuni  4219  uniintsn  4265  iununi  4359  unisn2  4530  opswap  5311  unixp0  5358  unixpid  5359  unizlim  5526  iotanul  5548  funfv  5916  dffv2  5922  1stval  6786  2ndval  6787  1stnpr  6788  2ndnpr  6789  1st0  6790  2nd0  6791  1st2val  6810  2nd2val  6811  brtpos0  6965  tpostpos  6978  nnunifi  7805  supval2  7948  infeq5  8087  rankuni  8313  rankxplim3  8331  iunfictbso  8527  cflim2  8675  fin1a2lem11  8822  itunisuc  8831  itunitc  8833  ttukeylem4  8924  incexclem  13799  arwval  15646  dprdsn  17403  zrhval  18845  0opn  19705  indistopon  19794  mretopd  19886  hauscmplem  20199  cmpfi  20201  comppfsc  20325  alexsublem  20836  alexsubALTlem2  20840  ptcmplem2  20845  lebnumlem3  21755  locfinref  28297  prsiga  28579  sigapildsys  28610  dya2iocuni  28731  fiunelcarsg  28764  carsgclctunlem1  28765  carsgclctunlem3  28768  unisnif  30263  limsucncmpi  30677  heicant  31421  ovoliunnfl  31428  voliunnfl  31430  volsupnfl  31431  mbfresfi  31433  stoweidlem35  37185  stoweidlem39  37189