Theorem uni0 4940

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

Assertion

Ref	Expression
uni0	⊢ ∪ ∅ = ∅

Proof of Theorem uni0

Step	Hyp	Ref	Expression
1		0ss 4397	. 2 ⊢ ∅ ⊆ {∅}
2		uni0b 4938	. 2 ⊢ (∪ ∅ = ∅ ↔ ∅ ⊆ {∅})
3	1, 2	mpbir 230	1 ⊢ ∪ ∅ = ∅

Syntax hints:   = wceq 1542   ⊆ wss 3949  ∅c0 4323  {csn 4629  ∪ cuni 4909

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-11 2155  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-rex 3072  df-v 3477  df-dif 3952  df-in 3956  df-ss 3966  df-nul 4324  df-sn 4630  df-uni 4910

This theorem is referenced by:  csbuni  4941  uniintsn  4992  iununi  5103  unisn2  5313  eqsnuniex  5360  opswap  6229  unixp0  6283  unixpid  6284  unizlim  6488  iotanul  6522  funfv  6979  dffv2  6987  1stval  7977  2ndval  7978  1stnpr  7979  2ndnpr  7980  1st0  7981  2nd0  7982  1st2val  8003  2nd2val  8004  brtpos0  8218  tpostpos  8231  nnunifi  9294  supval2  9450  sup00  9459  infeq5  9632  rankuni  9858  rankxplim3  9876  iunfictbso  10109  cflim2  10258  fin1a2lem11  10405  itunisuc  10414  itunitc  10416  ttukeylem4  10507  relexpfldd  14997  incexclem  15782  arwval  17993  dprdsn  19906  zrhval  21057  0opn  22406  indistopon  22504  mretopd  22596  hauscmplem  22910  cmpfi  22912  comppfsc  23036  alexsublem  23548  alexsubALTlem2  23552  ptcmplem2  23557  lebnumlem3  24479  old0  27354  made0  27368  locfinref  32821  prsiga  33129  sigapildsys  33160  dya2iocuni  33282  fiunelcarsg  33315  carsgclctunlem1  33316  carsgclctunlem3  33319  nnuni  34696  unisnif  34897  limsucncmpi  35330  heicant  36523  ovoliunnfl  36530  voliunnfl  36532  volsupnfl  36533  mbfresfi  36534  onov0suclim  42024  stoweidlem35  44751  stoweidlem39  44755  prsal  45034  issalnnd  45061  ismeannd  45183  caragenunicl  45240  isomennd  45247  ipolub0  47617