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  17584  smndex1basss  18808  smndex1mgm  18810  opsrtoslem2  21939  restcld  23035  neitr  23043  fiuncmp  23267  refun0  23378  1stckgenlem  23416  filconn  23746  ufildr  23794  alexsubALTlem3  23912  ptcmplem1  23915  restmetu  24434  ovolfiniun  25378  unmbl  25414  volfiniun  25424  voliunlem1  25427  plyun0  26078  lgsquadlem3  27269  noextend  27554  noextendseq  27555  nosupbday  27593  nosupbnd1  27602  nosupbnd2  27604  noinfbday  27608  noinfbnd1  27617  noinfbnd2  27619  noetasuplem2  27622  noetasuplem3  27623  noetasuplem4  27624  noetainflem4  27628  madeun  27771  addsproplem2  27853  addsasslem1  27886  addsasslem2  27887  negsproplem2  27911  negsproplem6  27915  negsid  27923  mulsproplem2  27996  mulsproplem3  27997  mulsproplem4  27998  mulsproplem12  28006  mulsproplem13  28007  mulsproplem14  28008  mulsass  28045  precsexlemcbv  28084  onmulscl  28151  axlowdimlem3  28847  axlowdimlem17  28861  ex-un  30326  ex-pw  30331  indifundif  32426  iuninc  32462  difico  32679  esum2dlem  34055  fiunelcarsg  34280  carsgclctunlem1  34281  carsggect  34282  bnj601  34883  bnj1416  35002  subfacp1lem1  35139  cvmliftlem10  35254  satf0  35332  poimirlem4  37591  poimirlem18  37605  poimirlem21  37608  poimirlem22  37609  poimirlem25  37612  mbfresfi  37633  asindmre  37670  fsuppssind  42554  mapfzcons  42677  mapfzcons1  42678  diophin  42733  iocunico  43173  rp-fakeuninass  43478  rclexi  43577  rtrclex  43579  dfrtrcl5  43591  dfrcl2  43636  corcltrcl  43701  cotrclrcl  43704  frege109d  43719  frege131d  43726  nregmodelf1o  44978  fiiuncl  45032  cnrefiisp  45801  fourierdlem65  46142  fourierdlem89  46166  fourierdlem90  46167  fourierdlem91  46168  fourierdlem96  46173  fourierdlem97  46174  fourierdlem98  46175  fourierdlem99  46176  fourierdlem100  46177  fourierdlem105  46182  fourierdlem108  46185  fourierdlem109  46186  fourierdlem110  46187  fourierdlem112  46189  fourierdlem113  46190  isomenndlem  46501  hoidmvlelem3  46568  1fzopredsuc  47298  dfclnbgr4  47798  clnbupgr  47807  usgrexmpl2edg  47993  lmod1zr  48455  dftpos5  48835  dftpos6  48836  tposresg  48839  tposrescnv  48840  tposres3  48842