Theorem uneq2i 4124

Description: Inference adding union to the left in a class equality. (Contributed by NM, 30-Aug-1993.)

Hypothesis

Ref	Expression
uneq1i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
uneq2i	⊢ (𝐶 ∪ 𝐴) = (𝐶 ∪ 𝐵)

Proof of Theorem uneq2i

Step	Hyp	Ref	Expression
1		uneq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		uneq2 4121	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∪ 𝐴) = (𝐶 ∪ 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐶 ∪ 𝐴) = (𝐶 ∪ 𝐵)

Syntax hints:   = wceq 1540   ∪ cun 3909

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-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-un 3916

This theorem is referenced by:  un4  4134  unundir  4136  difdif2  4255  difun2  4440  difdifdir  4451  dfif5  4501  qdass  4713  qdassr  4714  ssunpr  4794  iununi  5058  unidif0  5310  difxp1  6126  iunsuc  6407  fresaun  6713  fresaunres2  6714  fvssunirnOLD  6874  fmptap  7126  fvsnun1  7138  funiunfv  7204  onuninsuci  7796  frrlem14  8255  tfrlem10  8332  oarec  8503  dfdom2  8926  fodomr  9069  fodomfir  9255  ranksuc  9794  kmlem3  10082  djuassen  10108  fin1a2lem10  10338  fin1a2lem12  10340  axdc3lem4  10382  prunioo  13418  fz0sn0fz1  13582  facnn  14216  fac0  14217  hashun3  14325  trclublem  14937  dmtrclfv  14960  fsum2dlem  15712  fsumiun  15763  incexclem  15778  fprod2dlem  15922  prmreclem4  16866  phlstr  17285  mreexexlem4d  17588  smndex1basss  18814  smndex1mgm  18816  opsrtoslem2  21996  restcld  23092  neitr  23100  fiuncmp  23324  refun0  23435  1stckgenlem  23473  filconn  23803  ufildr  23851  alexsubALTlem3  23969  ptcmplem1  23972  restmetu  24491  ovolfiniun  25435  unmbl  25471  volfiniun  25481  voliunlem1  25484  plyun0  26135  lgsquadlem3  27326  noextend  27611  noextendseq  27612  nosupbday  27650  nosupbnd1  27659  nosupbnd2  27661  noinfbday  27665  noinfbnd1  27674  noinfbnd2  27676  noetasuplem2  27679  noetasuplem3  27680  noetasuplem4  27681  noetainflem4  27685  madeun  27833  addsproplem2  27917  addsasslem1  27950  addsasslem2  27951  negsproplem2  27975  negsproplem6  27979  negsid  27987  mulsproplem2  28060  mulsproplem3  28061  mulsproplem4  28062  mulsproplem12  28070  mulsproplem13  28071  mulsproplem14  28072  mulsass  28109  precsexlemcbv  28148  onmulscl  28215  axlowdimlem3  28924  axlowdimlem17  28938  ex-un  30403  ex-pw  30408  indifundif  32503  iuninc  32539  difico  32756  esum2dlem  34075  fiunelcarsg  34300  carsgclctunlem1  34301  carsggect  34302  bnj601  34903  bnj1416  35022  subfacp1lem1  35159  cvmliftlem10  35274  satf0  35352  poimirlem4  37611  poimirlem18  37625  poimirlem21  37628  poimirlem22  37629  poimirlem25  37632  mbfresfi  37653  asindmre  37690  fsuppssind  42574  mapfzcons  42697  mapfzcons1  42698  diophin  42753  iocunico  43193  rp-fakeuninass  43498  rclexi  43597  rtrclex  43599  dfrtrcl5  43611  dfrcl2  43656  corcltrcl  43721  cotrclrcl  43724  frege109d  43739  frege131d  43746  nregmodelf1o  44998  fiiuncl  45052  cnrefiisp  45821  fourierdlem65  46162  fourierdlem89  46186  fourierdlem90  46187  fourierdlem91  46188  fourierdlem96  46193  fourierdlem97  46194  fourierdlem98  46195  fourierdlem99  46196  fourierdlem100  46197  fourierdlem105  46202  fourierdlem108  46205  fourierdlem109  46206  fourierdlem110  46207  fourierdlem112  46209  fourierdlem113  46210  isomenndlem  46521  hoidmvlelem3  46588  1fzopredsuc  47318  dfclnbgr4  47818  clnbupgr  47827  usgrexmpl2edg  48013  lmod1zr  48475  dftpos5  48855  dftpos6  48856  tposresg  48859  tposrescnv  48860  tposres3  48862