Theorem uni0 4267

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

Syntax hints:   = wceq 1374   C_ wss 3471   (/)c0 3780   {csn 4022   U.cuni 4240

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1963  ax-ext 2440

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2612  df-ne 2659  df-ral 2814  df-rex 2815  df-v 3110  df-dif 3474  df-in 3478  df-ss 3485  df-nul 3781  df-sn 4023  df-uni 4241

This theorem is referenced by:  csbuni  4268  uniintsn  4314  iununi  4405  unisn2  4578  unizlim  4989  opswap  5488  unixp0  5534  unixpid  5535  iotanul  5559  funfv  5927  dffv2  5933  1stval  6778  2ndval  6779  1stnpr  6780  2ndnpr  6781  1st0  6782  2nd0  6783  1st2val  6802  2nd2val  6803  brtpos0  6954  tpostpos  6967  nnunifi  7762  supval2  7906  infeq5  8045  rankuni  8272  rankxplim3  8290  iunfictbso  8486  cflim2  8634  fin1a2lem11  8781  itunisuc  8790  itunitc  8792  ttukeylem4  8883  incexclem  13602  arwval  15219  dprdsn  16868  zrhval  18307  0opn  19175  indistopon  19263  mretopd  19354  hauscmplem  19667  cmpfi  19669  alexsublem  20274  alexsubALTlem2  20278  ptcmplem2  20283  lebnumlem3  21193  prsiga  27759  dya2iocuni  27882  unisnif  29140  limsucncmpi  29475  heicant  29615  ovoliunnfl  29622  voliunnfl  29624  volsupnfl  29625  mbfresfi  29627  comppfsc  29768  stoweidlem35  31292  stoweidlem39  31296