Theorem uni0 4276

Description: The union of the empty set is the empty set. Theorem 8.7 of [Quine] p. 54. (Reproved without relying on ax-nul 4581 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 3814	. 2
2		uni0b 4274	. 2
3	1, 2	mpbir 209	1

Syntax hints:  =wceq 1395  C_wss 3475  c0 3784  {csn 4029  U.cuni 4249

This theorem is referenced by:  csbuni  4277  uniintsn  4324  iununi  4415  unisn2  4588  unizlim  4999  opswap  5500  unixp0  5546  unixpid  5547  iotanul  5571  funfv  5940  dffv2  5946  1stval  6802  2ndval  6803  1stnpr  6804  2ndnpr  6805  1st0  6806  2nd0  6807  1st2val  6826  2nd2val  6827  brtpos0  6981  tpostpos  6994  nnunifi  7791  supval2  7935  infeq5  8075  rankuni  8302  rankxplim3  8320  iunfictbso  8516  cflim2  8664  fin1a2lem11  8811  itunisuc  8820  itunitc  8822  ttukeylem4  8913  incexclem  13648  arwval  15370  dprdsn  17083  zrhval  18545  0opn  19413  indistopon  19502  mretopd  19593  hauscmplem  19906  cmpfi  19908  comppfsc  20033  alexsublem  20544  alexsubALTlem2  20548  ptcmplem2  20553  lebnumlem3  21463  locfinref  27844  prsiga  28131  dya2iocuni  28254  unisnif  29575  limsucncmpi  29910  heicant  30049  ovoliunnfl  30056  voliunnfl  30058  volsupnfl  30059  mbfresfi  30061  stoweidlem35  31817  stoweidlem39  31821

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-v 3111  df-dif 3478  df-in 3482  df-ss 3489  df-nul 3785  df-sn 4030  df-uni 4250