Theorem un0 4351

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 4293	. . . 4 ⊢ ¬ 𝑥 ∈ ∅
2	1	biorfri 952	. . 3 ⊢ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ ∅))
3	2	bicomi 227	. 2 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ ∅) ↔ 𝑥 ∈ 𝐴)
4	3	uneqri 4112	1 ⊢ (𝐴 ∪ ∅) = 𝐴

Syntax hints:   ∨ wo 860   = wceq 1563   ∈ wcel 2145   ∪ cun 3905  ∅c0 4288

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-dif 3910  df-un 3912  df-nul 4289

This theorem is referenced by:  0un  4353  csbun  4398  un00  4402  disjssun  4425  difun2  4438  difdifdir  4448  disjpr2  4675  prprc1  4727  diftpsn3  4765  symdif0  5047  symdifid  5049  iununi  5061  unidif0  5321  unidif0OLD  5322  relresdm1  6026  difxp1  6154  difxp2  6155  suc0  6427  sucprc  6428  fresaun  6739  fresaunres2  6740  fvun1  6962  fndifnfp  7164  fvunsn  7167  fvsnun1  7170  fvsnun2  7171  fsnunfv  7175  fsnunres  7176  funiunfv  7236  fnsuppeq0  8176  frrlem12  8282  oev2  8496  oarec  8535  undifixp  8920  domss2  9112  unfi  9143  domunfican  9269  kmlem2  10123  kmlem3  10124  kmlem11  10132  dju0en  10147  djuassen  10150  ackbij1lem1  10190  ackbij1lem13  10202  fin1a2lem10  10381  fin1a2lem12  10383  axdc3lem4  10425  ttukeylem6  10486  alephadd  10550  fpwwe2lem12  10615  indconst1  12222  prunioo  13499  fzsuc2  13601  fseq1p1m1  13617  hashgval  14360  hashinf  14362  hashfun  14464  sadid1  16516  lcmfunsnlem  16689  lcmfun  16693  vdwap1  17027  setsres  17228  setsid  17257  mreexexlem3d  17692  mreexdomd  17695  pwmndid  18988  pwmnd  18989  pwssplit1  21149  lspsnat  21238  lsppratlem3  21242  opsrtoslem2  22167  indistopon  23119  indistps  23129  indistps2  23130  restcld  23290  neitr  23298  refun0  23633  filconn  24001  ufildr  24049  restmetu  24688  ovolioo  25688  itgsplitioo  25958  plyeq0  26329  birthdaylem2  27075  lgsquadlem2  27503  noextendseq  27789  nosupbnd2lem1  27837  noinfbnd2lem1  27852  noetasuplem2  27856  noetasuplem3  27857  noetasuplem4  27858  noetainflem2  27860  bday1  27965  lrold  28048  addsrid  28115  negsproplem2  28180  negsproplem6  28184  muls01  28263  mulsrid  28264  mulsproplem2  28268  mulsproplem3  28269  mulsproplem4  28270  mulsproplem12  28278  mulsproplem13  28279  mulsproplem14  28280  onleft  28411  ltonold  28412  oncutlt  28415  oniso  28422  bdayons  28427  onaddscl  28428  onmulscl  28429  n0cut  28485  n0bday  28503  bdayn0p1  28520  0reno  28647  1reno  28648  ex-dif  30683  ex-in  30685  ex-res  30701  difres  32855  imadifxp  32856  ofpreima2  32923  coprprop  32956  padct  32975  difico  33040  tocycf  33350  tocyc01  33351  elrgspnlem4  33478  esplyind  33882  constrextdg2lem  34055  locfinref  34148  sigaclfu2  34428  prsiga  34438  unelldsys  34465  measun  34518  difelcarsg  34617  carsgclctunlem1  34624  carsggect  34625  eulerpartlemt  34678  eulerpartgbij  34679  ballotlemfp1  34799  fineqvac  35424  indispconn  35597  onint1  36822  bj-pr21val  37510  bj-funun  37756  lindsdom  38125  poimirlem3  38134  poimirlem5  38136  poimirlem10  38141  poimirlem15  38146  poimirlem22  38153  poimirlem23  38154  poimirlem28  38159  padd01  40447  padd02  40448  pclfinclN  40586  mapfzcons1  43310  fzsplit1nn0  43347  diophrw  43352  eldioph2lem1  43353  eldioph2lem2  43354  diophren  43402  pwssplit4  43678  mnuprdlem1  44846  dvmptfprodlem  46516  caratheodorylem1  47098  isomenndlem  47102  fzopredsuc  47916  clnbgr0edg  48457  tposrescnv  49508  tposres2  49509  tposres3  49510  aacllem  50430