Theorem uni0 4195

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

Syntax hints:   = wceq 1448   C_ wss 3372   (/)c0 3699   {csn 3936   U.cuni 4168

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1673  ax-4 1686  ax-5 1762  ax-6 1809  ax-7 1855  ax-10 1919  ax-11 1924  ax-12 1937  ax-13 2092  ax-ext 2432

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1451  df-ex 1668  df-nf 1672  df-sb 1802  df-clab 2439  df-cleq 2445  df-clel 2448  df-nfc 2582  df-ne 2624  df-ral 2742  df-rex 2743  df-v 3015  df-dif 3375  df-in 3379  df-ss 3386  df-nul 3700  df-sn 3937  df-uni 4169

This theorem is referenced by:  csbuni  4196  uniintsn  4242  iununi  4338  unisn2  4511  opswap  5302  unixp0  5349  unixpid  5350  unizlim  5518  iotanul  5540  funfv  5916  dffv2  5922  1stval  6783  2ndval  6784  1stnpr  6785  2ndnpr  6786  1st0  6787  2nd0  6788  1st2val  6807  2nd2val  6808  brtpos0  6967  tpostpos  6980  nnunifi  7809  supval2  7956  sup00  7965  infeq5  8129  rankuni  8321  rankxplim3  8339  iunfictbso  8532  cflim2  8680  fin1a2lem11  8827  itunisuc  8836  itunitc  8838  ttukeylem4  8929  incexclem  13905  arwval  15949  dprdsn  17680  zrhval  19090  0opn  19945  indistopon  20027  mretopd  20119  hauscmplem  20432  cmpfi  20434  comppfsc  20558  alexsublem  21070  alexsubALTlem2  21074  ptcmplem2  21079  lebnumlem3  22002  lebnumlem3OLD  22005  locfinref  28675  prsiga  28960  sigapildsys  28991  dya2iocuni  29111  fiunelcarsg  29154  carsgclctunlem1  29155  carsgclctunlem3  29158  unisnif  30698  limsucncmpi  31111  heicant  31977  ovoliunnfl  31984  voliunnfl  31986  volsupnfl  31987  mbfresfi  31989  stoweidlem35  37953  stoweidlem39  37957  prsal  38236  issalnnd  38261  ismeannd  38366  caragenunicl  38409  isomennd  38416