Theorem uneq2i 4106

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 4103	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∪ 𝐴) = (𝐶 ∪ 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐶 ∪ 𝐴) = (𝐶 ∪ 𝐵)

Syntax hints:   = wceq 1542   ∪ cun 3888

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-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-un 3895

This theorem is referenced by:  un4  4116  unundir  4118  difdif2  4237  difun2  4422  difdifdir  4432  dfif5  4484  qdass  4698  qdassr  4699  ssunpr  4778  iununi  5042  unidif0  5295  difxp1  6121  iunsuc  6402  fresaun  6703  fresaunres2  6704  fmptap  7116  fvsnun1  7128  funiunfv  7194  onuninsuci  7782  frrlem14  8240  tfrlem10  8317  oarec  8488  dfdom2  8916  fodomr  9057  fodomfir  9229  ranksuc  9778  kmlem3  10064  djuassen  10090  fin1a2lem10  10320  fin1a2lem12  10322  axdc3lem4  10364  prunioo  13423  fz0sn0fz1  13588  facnn  14226  fac0  14227  hashun3  14335  trclublem  14946  dmtrclfv  14969  fsum2dlem  15721  fsumiun  15773  incexclem  15790  fprod2dlem  15934  prmreclem4  16879  phlstr  17298  mreexexlem4d  17602  smndex1basss  18865  smndex1mgm  18867  opsrtoslem2  22043  restcld  23146  neitr  23154  fiuncmp  23378  refun0  23489  1stckgenlem  23527  filconn  23857  ufildr  23905  alexsubALTlem3  24023  ptcmplem1  24026  restmetu  24544  ovolfiniun  25477  unmbl  25513  volfiniun  25523  voliunlem1  25526  plyun0  26174  lgsquadlem3  27364  noextend  27649  noextendseq  27650  nosupbday  27688  nosupbnd1  27697  nosupbnd2  27699  noinfbday  27703  noinfbnd1  27712  noinfbnd2  27714  noetasuplem2  27717  noetasuplem3  27718  noetasuplem4  27719  noetainflem4  27723  madeun  27895  addsproplem2  27981  addsasslem1  28014  addsasslem2  28015  negsproplem2  28040  negsproplem6  28044  negsid  28052  mulsproplem2  28128  mulsproplem3  28129  mulsproplem4  28130  mulsproplem12  28138  mulsproplem13  28139  mulsproplem14  28140  mulsass  28177  precsexlemcbv  28217  onmulscl  28289  axlowdimlem3  29032  axlowdimlem17  29046  ex-un  30514  ex-pw  30519  indifundif  32614  iuninc  32650  difico  32876  esum2dlem  34257  fiunelcarsg  34481  carsgclctunlem1  34482  carsggect  34483  bnj601  35083  bnj1416  35202  subfacp1lem1  35382  cvmliftlem10  35497  satf0  35575  poimirlem4  37956  poimirlem18  37970  poimirlem21  37973  poimirlem22  37974  poimirlem25  37977  mbfresfi  37998  asindmre  38035  dmuncnvepres  38723  blockadjliftmap  38790  fsuppssind  43037  mapfzcons  43159  mapfzcons1  43160  diophin  43215  iocunico  43654  rp-fakeuninass  43958  rclexi  44057  rtrclex  44059  dfrtrcl5  44071  dfrcl2  44116  corcltrcl  44181  cotrclrcl  44184  frege109d  44199  frege131d  44206  nregmodelf1o  45457  fiiuncl  45511  cnrefiisp  46273  fourierdlem65  46614  fourierdlem89  46638  fourierdlem90  46639  fourierdlem91  46640  fourierdlem96  46645  fourierdlem97  46646  fourierdlem98  46647  fourierdlem99  46648  fourierdlem100  46649  fourierdlem105  46654  fourierdlem108  46657  fourierdlem109  46658  fourierdlem110  46659  fourierdlem112  46661  fourierdlem113  46662  isomenndlem  46973  hoidmvlelem3  47040  1fzopredsuc  47770  dfclnbgr4  48297  clnbupgr  48306  usgrexmpl2edg  48502  lmod1zr  48966  dftpos5  49346  dftpos6  49347  tposresg  49350  tposrescnv  49351  tposres3  49353