Theorem uni0 4465

Description: The union of the empty set is the empty set. Theorem 8.7 of [Quine] p. 54. (Reproved without relying on ax-nul 4789 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 3972	. 2 ⊢ ∅ ⊆ {∅}
2		uni0b 4463	. 2 ⊢ (∪ ∅ = ∅ ↔ ∅ ⊆ {∅})
3	1, 2	mpbir 221	1 ⊢ ∪ ∅ = ∅

Syntax hints:   = wceq 1483   ⊆ wss 3574  ∅c0 3915  {csn 4177  ∪ cuni 4436

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-v 3202  df-dif 3577  df-in 3581  df-ss 3588  df-nul 3916  df-sn 4178  df-uni 4437

This theorem is referenced by:  csbuni  4466  uniintsn  4514  iununi  4610  unisn2  4794  opswap  5622  unixp0  5669  unixpid  5670  unizlim  5844  iotanul  5866  funfv  6265  dffv2  6271  1stval  7170  2ndval  7171  1stnpr  7172  2ndnpr  7173  1st0  7174  2nd0  7175  1st2val  7194  2nd2val  7195  brtpos0  7359  tpostpos  7372  nnunifi  8211  supval2  8361  sup00  8370  infeq5  8534  rankuni  8726  rankxplim3  8744  iunfictbso  8937  cflim2  9085  fin1a2lem11  9232  itunisuc  9241  itunitc  9243  ttukeylem4  9334  incexclem  14568  arwval  16693  dprdsn  18435  zrhval  19856  0opn  20709  indistopon  20805  mretopd  20896  hauscmplem  21209  cmpfi  21211  comppfsc  21335  alexsublem  21848  alexsubALTlem2  21852  ptcmplem2  21857  lebnumlem3  22762  locfinref  29908  prsiga  30194  sigapildsys  30225  dya2iocuni  30345  fiunelcarsg  30378  carsgclctunlem1  30379  carsgclctunlem3  30382  unisnif  32032  limsucncmpi  32444  heicant  33444  ovoliunnfl  33451  voliunnfl  33453  volsupnfl  33454  mbfresfi  33456  stoweidlem35  40252  stoweidlem39  40256  prsal  40538  issalnnd  40563  ismeannd  40684  caragenunicl  40738  isomennd  40745