Theorem un0 4344

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 4288	. . . 4 ⊢ ¬ 𝑥 ∈ ∅
2	1	biorfri 939	. . 3 ⊢ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ ∅))
3	2	bicomi 224	. 2 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ ∅) ↔ 𝑥 ∈ 𝐴)
4	3	uneqri 4106	1 ⊢ (𝐴 ∪ ∅) = 𝐴

Syntax hints:   ∨ wo 847   = wceq 1541   ∈ wcel 2111   ∪ cun 3900  ∅c0 4283

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-dif 3905  df-un 3907  df-nul 4284

This theorem is referenced by:  0un  4346  csbun  4391  un00  4395  disjssun  4418  difun2  4431  difdifdir  4442  disjpr2  4666  prprc1  4718  diftpsn3  4754  sspr  4787  sstp  4788  symdif0  5033  symdifv  5034  symdifid  5035  iunxdif3  5043  iununi  5047  unidif0  5298  relresdm1  5982  difxp1  6112  difxp2  6113  suc0  6383  sucprc  6384  fresaun  6694  fresaunres2  6695  fvun1  6913  fndifnfp  7110  fvunsn  7113  fvsnun1  7116  fvsnun2  7117  fsnunfv  7121  fsnunres  7122  funiunfv  7182  fnsuppeq0  8122  frrlem12  8227  oev2  8438  oarec  8477  undifixp  8858  domss2  9049  unfi  9080  domunfican  9206  kmlem2  10040  kmlem3  10041  kmlem11  10049  dju0en  10064  djuassen  10067  ackbij1lem1  10107  ackbij1lem13  10119  fin1a2lem10  10297  fin1a2lem12  10299  axdc3lem4  10341  ttukeylem6  10402  alephadd  10465  fpwwe2lem12  10530  prunioo  13378  fzsuc2  13479  fseq1p1m1  13495  hashgval  14237  hashinf  14239  hashfun  14341  sadid1  16376  lcmfunsnlem  16549  lcmfun  16553  vdwap1  16886  setsres  17086  setsid  17115  mreexexlem3d  17549  mreexdomd  17552  pwmndid  18841  pwmnd  18842  pwssplit1  20991  lspsnat  21080  lsppratlem3  21084  opsrtoslem2  21989  indistopon  22914  indistps  22924  indistps2  22925  restcld  23085  neitr  23093  refun0  23428  filconn  23796  ufildr  23844  restmetu  24483  ovolioo  25494  itgsplitioo  25764  plyeq0  26141  birthdaylem2  26887  lgsquadlem2  27317  noextendseq  27604  nosupbnd2lem1  27652  noinfbnd2lem1  27667  noetasuplem2  27671  noetasuplem3  27672  noetasuplem4  27673  noetainflem2  27675  bday1s  27773  lrold  27840  addsrid  27905  negsproplem2  27969  negsproplem6  27973  muls01  28049  mulsrid  28050  mulsproplem2  28054  mulsproplem3  28055  mulsproplem4  28056  mulsproplem12  28064  mulsproplem13  28065  mulsproplem14  28066  onsleft  28195  sltonold  28196  onscutlt  28199  onsiso  28203  bdayon  28207  onaddscl  28208  onmulscl  28209  n0scut  28260  n0sbday  28278  bdayn0p1  28292  ex-dif  30398  ex-in  30400  ex-res  30416  difres  32575  imadifxp  32576  ofpreima2  32643  coprprop  32675  padct  32696  difico  32761  tocycf  33081  tocyc01  33082  elrgspnlem4  33207  constrextdg2lem  33756  locfinref  33849  sigaclfu2  34129  prsiga  34139  unelldsys  34166  measun  34219  difelcarsg  34318  carsgclctunlem1  34325  carsggect  34326  eulerpartlemt  34379  eulerpartgbij  34380  ballotlemfp1  34500  fineqvac  35127  indispconn  35266  onint1  36482  bj-pr21val  37046  bj-funun  37285  lindsdom  37653  poimirlem3  37662  poimirlem5  37664  poimirlem10  37669  poimirlem15  37674  poimirlem22  37681  poimirlem23  37682  poimirlem28  37687  padd01  39849  padd02  39850  pclfinclN  39988  mapfzcons1  42749  fzsplit1nn0  42786  diophrw  42791  eldioph2lem1  42792  eldioph2lem2  42793  diophren  42845  pwssplit4  43121  mnuprdlem1  44304  dvmptfprodlem  45981  caratheodorylem1  46563  isomenndlem  46567  fzopredsuc  47353  clnbgr0edg  47867  tposrescnv  48909  tposres2  48910  tposres3  48911  aacllem  49832