Theorem un0 4391

Description: The union of a class with the empty set is itself. Theorem 24 of [Suppes] p. 27. (Contributed by NM, 15-Jul-1993.)

Assertion

Ref	Expression
un0	⊢ (𝐴 ∪ ∅) = 𝐴

Proof of Theorem un0

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		noel 4331	. . . 4 ⊢ ¬ 𝑥 ∈ ∅
2	1	biorfi 938	. . 3 ⊢ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ ∅))
3	2	bicomi 223	. 2 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ ∅) ↔ 𝑥 ∈ 𝐴)
4	3	uneqri 4152	1 ⊢ (𝐴 ∪ ∅) = 𝐴

Syntax hints:   ∨ wo 846   = wceq 1542   ∈ wcel 2107   ∪ cun 3947  ∅c0 4323

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-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-dif 3952  df-un 3954  df-nul 4324

This theorem is referenced by:  0un  4393  csbun  4439  un00  4443  disjssun  4468  difun2  4481  difdifdir  4492  disjpr2  4718  prprc1  4770  diftpsn3  4806  sspr  4837  sstp  4838  symdif0  5089  symdifv  5090  symdifid  5091  iunxdif3  5099  iununi  5103  unidif0  5359  relresdm1  6034  difxp1  6165  difxp2  6166  suc0  6440  sucprc  6441  fresaun  6763  fresaunres2  6764  fvssunirnOLD  6926  fvun1  6983  fndifnfp  7174  fvunsn  7177  fvsnun1  7180  fvsnun2  7181  fsnunfv  7185  fsnunres  7186  funiunfv  7247  fnsuppeq0  8177  frrlem12  8282  wfrlem14OLD  8322  oev2  8523  oarec  8562  undifixp  8928  domss2  9136  unfi  9172  domunfican  9320  kmlem2  10146  kmlem3  10147  kmlem11  10155  dju0en  10170  djuassen  10173  ackbij1lem1  10215  ackbij1lem13  10227  fin1a2lem10  10404  fin1a2lem12  10406  axdc3lem4  10448  ttukeylem6  10509  alephadd  10572  fpwwe2lem12  10637  prunioo  13458  fzsuc2  13559  fseq1p1m1  13575  hashgval  14293  hashinf  14295  hashfun  14397  sadid1  16409  lcmfunsnlem  16578  lcmfun  16582  vdwap1  16910  setsres  17111  setsid  17141  mreexexlem3d  17590  mreexdomd  17593  pwmndid  18817  pwmnd  18818  pwssplit1  20670  lspsnat  20758  lsppratlem3  20762  opsrtoslem2  21617  indistopon  22504  indistps  22514  indistps2  22515  restcld  22676  neitr  22684  refun0  23019  filconn  23387  ufildr  23435  restmetu  24079  ovolioo  25085  itgsplitioo  25355  plyeq0  25725  birthdaylem2  26457  lgsquadlem2  26884  noextendseq  27170  nosupbnd2lem1  27218  noinfbnd2lem1  27233  noetasuplem2  27237  noetasuplem3  27238  noetasuplem4  27239  noetainflem2  27241  bday1s  27332  lrold  27391  addsrid  27448  negsproplem2  27503  negsproplem6  27507  muls01  27568  mulsrid  27569  mulsproplem2  27573  mulsproplem3  27574  mulsproplem4  27575  mulsproplem12  27583  mulsproplem13  27584  mulsproplem14  27585  ex-dif  29676  ex-in  29678  ex-res  29694  difres  31831  imadifxp  31832  ofpreima2  31891  coprprop  31921  padct  31944  difico  31994  tocycf  32276  tocyc01  32277  locfinref  32821  sigaclfu2  33119  prsiga  33129  unelldsys  33156  measun  33209  difelcarsg  33309  carsgclctunlem1  33316  carsggect  33317  eulerpartlemt  33370  eulerpartgbij  33371  ballotlemfp1  33490  fineqvac  34097  indispconn  34225  onint1  35334  bj-pr21val  35894  bj-funun  36133  lindsdom  36482  poimirlem3  36491  poimirlem5  36493  poimirlem10  36498  poimirlem15  36503  poimirlem22  36510  poimirlem23  36511  poimirlem28  36516  padd01  38682  padd02  38683  pclfinclN  38821  metakunt24  41008  mapfzcons1  41455  fzsplit1nn0  41492  diophrw  41497  eldioph2lem1  41498  eldioph2lem2  41499  diophren  41551  pwssplit4  41831  mnuprdlem1  43031  dvmptfprodlem  44660  caratheodorylem1  45242  isomenndlem  45246  fzopredsuc  46031  aacllem  47848