Theorem un0 4348

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

Syntax hints:   ∨ wo 848   = wceq 1542   ∈ wcel 2114   ∪ cun 3901  ∅c0 4287

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-dif 3906  df-un 3908  df-nul 4288

This theorem is referenced by:  0un  4350  csbun  4395  un00  4399  disjssun  4422  difun2  4435  difdifdir  4446  disjpr2  4672  prprc1  4724  diftpsn3  4760  sspr  4793  sstp  4794  symdif0  5042  symdifv  5043  symdifid  5044  iunxdif3  5052  iununi  5056  unidif0  5307  relresdm1  6000  difxp1  6131  difxp2  6132  suc0  6402  sucprc  6403  fresaun  6713  fresaunres2  6714  fvun1  6933  fndifnfp  7132  fvunsn  7135  fvsnun1  7138  fvsnun2  7139  fsnunfv  7143  fsnunres  7144  funiunfv  7204  fnsuppeq0  8144  frrlem12  8249  oev2  8460  oarec  8499  undifixp  8884  domss2  9076  unfi  9107  domunfican  9234  kmlem2  10074  kmlem3  10075  kmlem11  10083  dju0en  10098  djuassen  10101  ackbij1lem1  10141  ackbij1lem13  10153  fin1a2lem10  10331  fin1a2lem12  10333  axdc3lem4  10375  ttukeylem6  10436  alephadd  10500  fpwwe2lem12  10565  prunioo  13409  fzsuc2  13510  fseq1p1m1  13526  hashgval  14268  hashinf  14270  hashfun  14372  sadid1  16407  lcmfunsnlem  16580  lcmfun  16584  vdwap1  16917  setsres  17117  setsid  17146  mreexexlem3d  17581  mreexdomd  17584  pwmndid  18873  pwmnd  18874  pwssplit1  21023  lspsnat  21112  lsppratlem3  21116  opsrtoslem2  22023  indistopon  22957  indistps  22967  indistps2  22968  restcld  23128  neitr  23136  refun0  23471  filconn  23839  ufildr  23887  restmetu  24526  ovolioo  25537  itgsplitioo  25807  plyeq0  26184  birthdaylem2  26930  lgsquadlem2  27360  noextendseq  27647  nosupbnd2lem1  27695  noinfbnd2lem1  27710  noetasuplem2  27714  noetasuplem3  27715  noetasuplem4  27716  noetainflem2  27718  bday1  27822  lrold  27905  addsrid  27972  negsproplem2  28037  negsproplem6  28041  muls01  28120  mulsrid  28121  mulsproplem2  28125  mulsproplem3  28126  mulsproplem4  28127  mulsproplem12  28135  mulsproplem13  28136  mulsproplem14  28137  onleft  28268  ltonold  28269  oncutlt  28272  oniso  28279  bdayons  28284  onaddscl  28285  onmulscl  28286  n0cut  28342  n0bday  28360  bdayn0p1  28377  0reno  28504  1reno  28505  ex-dif  30510  ex-in  30512  ex-res  30528  difres  32686  imadifxp  32687  ofpreima2  32755  coprprop  32788  padct  32807  difico  32873  indconst1  32950  tocycf  33210  tocyc01  33211  elrgspnlem4  33338  esplyind  33751  constrextdg2lem  33925  locfinref  34018  sigaclfu2  34298  prsiga  34308  unelldsys  34335  measun  34388  difelcarsg  34487  carsgclctunlem1  34494  carsggect  34495  eulerpartlemt  34548  eulerpartgbij  34549  ballotlemfp1  34669  fineqvac  35291  indispconn  35447  onint1  36662  bj-pr21val  37255  bj-funun  37501  lindsdom  37859  poimirlem3  37868  poimirlem5  37870  poimirlem10  37875  poimirlem15  37880  poimirlem22  37887  poimirlem23  37888  poimirlem28  37893  padd01  40181  padd02  40182  pclfinclN  40320  mapfzcons1  43068  fzsplit1nn0  43105  diophrw  43110  eldioph2lem1  43111  eldioph2lem2  43112  diophren  43164  pwssplit4  43440  mnuprdlem1  44622  dvmptfprodlem  46296  caratheodorylem1  46878  isomenndlem  46882  fzopredsuc  47677  clnbgr0edg  48191  tposrescnv  49232  tposres2  49233  tposres3  49234  aacllem  50154