Theorem un0 4357

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

Syntax hints:   ∨ wo 847   = wceq 1540   ∈ wcel 2109   ∪ cun 3912  ∅c0 4296

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-dif 3917  df-un 3919  df-nul 4297

This theorem is referenced by:  0un  4359  csbun  4404  un00  4408  disjssun  4431  difun2  4444  difdifdir  4455  disjpr2  4677  prprc1  4729  diftpsn3  4766  sspr  4799  sstp  4800  symdif0  5049  symdifv  5050  symdifid  5051  iunxdif3  5059  iununi  5063  unidif0  5315  relresdm1  6004  difxp1  6138  difxp2  6139  suc0  6409  sucprc  6410  fresaun  6731  fresaunres2  6732  fvssunirnOLD  6892  fvun1  6952  fndifnfp  7150  fvunsn  7153  fvsnun1  7156  fvsnun2  7157  fsnunfv  7161  fsnunres  7162  funiunfv  7222  fnsuppeq0  8171  frrlem12  8276  oev2  8487  oarec  8526  undifixp  8907  domss2  9100  unfi  9135  domunfican  9272  kmlem2  10105  kmlem3  10106  kmlem11  10114  dju0en  10129  djuassen  10132  ackbij1lem1  10172  ackbij1lem13  10184  fin1a2lem10  10362  fin1a2lem12  10364  axdc3lem4  10406  ttukeylem6  10467  alephadd  10530  fpwwe2lem12  10595  prunioo  13442  fzsuc2  13543  fseq1p1m1  13559  hashgval  14298  hashinf  14300  hashfun  14402  sadid1  16438  lcmfunsnlem  16611  lcmfun  16615  vdwap1  16948  setsres  17148  setsid  17177  mreexexlem3d  17607  mreexdomd  17610  pwmndid  18863  pwmnd  18864  pwssplit1  20966  lspsnat  21055  lsppratlem3  21059  opsrtoslem2  21963  indistopon  22888  indistps  22898  indistps2  22899  restcld  23059  neitr  23067  refun0  23402  filconn  23770  ufildr  23818  restmetu  24458  ovolioo  25469  itgsplitioo  25739  plyeq0  26116  birthdaylem2  26862  lgsquadlem2  27292  noextendseq  27579  nosupbnd2lem1  27627  noinfbnd2lem1  27642  noetasuplem2  27646  noetasuplem3  27647  noetasuplem4  27648  noetainflem2  27650  bday1s  27743  lrold  27808  addsrid  27871  negsproplem2  27935  negsproplem6  27939  muls01  28015  mulsrid  28016  mulsproplem2  28020  mulsproplem3  28021  mulsproplem4  28022  mulsproplem12  28030  mulsproplem13  28031  mulsproplem14  28032  onsleft  28161  sltonold  28162  onscutlt  28165  onsiso  28169  bdayon  28173  onaddscl  28174  onmulscl  28175  n0scut  28226  n0sbday  28244  bdayn0p1  28258  ex-dif  30352  ex-in  30354  ex-res  30370  difres  32529  imadifxp  32530  ofpreima2  32590  coprprop  32622  padct  32643  difico  32706  tocycf  33074  tocyc01  33075  elrgspnlem4  33196  constrextdg2lem  33738  locfinref  33831  sigaclfu2  34111  prsiga  34121  unelldsys  34148  measun  34201  difelcarsg  34301  carsgclctunlem1  34308  carsggect  34309  eulerpartlemt  34362  eulerpartgbij  34363  ballotlemfp1  34483  fineqvac  35087  indispconn  35221  onint1  36437  bj-pr21val  37001  bj-funun  37240  lindsdom  37608  poimirlem3  37617  poimirlem5  37619  poimirlem10  37624  poimirlem15  37629  poimirlem22  37636  poimirlem23  37637  poimirlem28  37642  padd01  39805  padd02  39806  pclfinclN  39944  mapfzcons1  42705  fzsplit1nn0  42742  diophrw  42747  eldioph2lem1  42748  eldioph2lem2  42749  diophren  42801  pwssplit4  43078  mnuprdlem1  44261  dvmptfprodlem  45942  caratheodorylem1  46524  isomenndlem  46528  fzopredsuc  47324  clnbgr0edg  47837  tposrescnv  48867  tposres2  48868  tposres3  48869  aacllem  49790