Theorem uni0 4623

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

Assertion

Ref	Expression
uni0	⊢ ∪ ∅ = ∅

Proof of Theorem uni0

Step	Hyp	Ref	Expression
1		0ss 4134	. 2 ⊢ ∅ ⊆ {∅}
2		uni0b 4621	. 2 ⊢ (∪ ∅ = ∅ ↔ ∅ ⊆ {∅})
3	1, 2	mpbir 222	1 ⊢ ∪ ∅ = ∅

Syntax hints:   = wceq 1652   ⊆ wss 3732  ∅c0 4079  {csn 4334  ∪ cuni 4594

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ral 3060  df-rex 3061  df-v 3352  df-dif 3735  df-in 3739  df-ss 3746  df-nul 4080  df-sn 4335  df-uni 4595

This theorem is referenced by:  csbuni  4624  uniintsn  4670  iununi  4767  unisn2  4955  opswap  5808  unixp0  5855  unixpid  5856  unizlim  6024  iotanul  6046  funfv  6454  dffv2  6460  1stval  7368  2ndval  7369  1stnpr  7370  2ndnpr  7371  1st0  7372  2nd0  7373  1st2val  7394  2nd2val  7395  brtpos0  7562  tpostpos  7575  nnunifi  8418  supval2  8568  sup00  8577  infeq5  8749  rankuni  8941  rankxplim3  8959  iunfictbso  9188  cflim2  9338  fin1a2lem11  9485  itunisuc  9494  itunitc  9496  ttukeylem4  9587  incexclem  14854  arwval  16960  dprdsn  18702  zrhval  20129  0opn  20988  indistopon  21085  mretopd  21176  hauscmplem  21489  cmpfi  21491  comppfsc  21615  alexsublem  22127  alexsubALTlem2  22131  ptcmplem2  22136  lebnumlem3  23041  locfinref  30290  prsiga  30576  sigapildsys  30607  dya2iocuni  30727  fiunelcarsg  30760  carsgclctunlem1  30761  carsgclctunlem3  30764  unisnif  32408  limsucncmpi  32815  heicant  33800  ovoliunnfl  33807  voliunnfl  33809  volsupnfl  33810  mbfresfi  33811  stoweidlem35  40821  stoweidlem39  40825  prsal  41107  issalnnd  41132  ismeannd  41253  caragenunicl  41310  isomennd  41317