Theorem uneq2i 4105

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

Syntax hints:   = wceq 1542   ∪ cun 3887

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-un 3894

This theorem is referenced by:  un4  4115  unundir  4117  difdif2  4236  difun2  4421  difdifdir  4431  dfif5  4483  qdass  4697  qdassr  4698  ssunpr  4777  iununi  5041  unidif0  5301  unidif0OLD  5302  difxp1  6129  iunsuc  6410  fresaun  6711  fresaunres2  6712  fmptap  7125  fvsnun1  7137  funiunfv  7203  onuninsuci  7791  frrlem14  8249  tfrlem10  8326  oarec  8497  dfdom2  8925  fodomr  9066  fodomfir  9238  ranksuc  9789  kmlem3  10075  djuassen  10101  fin1a2lem10  10331  fin1a2lem12  10333  axdc3lem4  10375  prunioo  13434  fz0sn0fz1  13599  facnn  14237  fac0  14238  hashun3  14346  trclublem  14957  dmtrclfv  14980  fsum2dlem  15732  fsumiun  15784  incexclem  15801  fprod2dlem  15945  prmreclem4  16890  phlstr  17309  mreexexlem4d  17613  smndex1basss  18876  smndex1mgm  18878  opsrtoslem2  22034  restcld  23137  neitr  23145  fiuncmp  23369  refun0  23480  1stckgenlem  23518  filconn  23848  ufildr  23896  alexsubALTlem3  24014  ptcmplem1  24017  restmetu  24535  ovolfiniun  25468  unmbl  25504  volfiniun  25514  voliunlem1  25517  plyun0  26162  lgsquadlem3  27345  noextend  27630  noextendseq  27631  nosupbday  27669  nosupbnd1  27678  nosupbnd2  27680  noinfbday  27684  noinfbnd1  27693  noinfbnd2  27695  noetasuplem2  27698  noetasuplem3  27699  noetasuplem4  27700  noetainflem4  27704  madeun  27876  addsproplem2  27962  addsasslem1  27995  addsasslem2  27996  negsproplem2  28021  negsproplem6  28025  negsid  28033  mulsproplem2  28109  mulsproplem3  28110  mulsproplem4  28111  mulsproplem12  28119  mulsproplem13  28120  mulsproplem14  28121  mulsass  28158  precsexlemcbv  28198  onmulscl  28270  axlowdimlem3  29013  axlowdimlem17  29027  ex-un  30494  ex-pw  30499  indifundif  32594  iuninc  32630  difico  32856  esum2dlem  34236  fiunelcarsg  34460  carsgclctunlem1  34461  carsggect  34462  bnj601  35062  bnj1416  35181  subfacp1lem1  35361  cvmliftlem10  35476  satf0  35554  poimirlem4  37945  poimirlem18  37959  poimirlem21  37962  poimirlem22  37963  poimirlem25  37966  mbfresfi  37987  asindmre  38024  dmuncnvepres  38712  blockadjliftmap  38779  fsuppssind  43026  mapfzcons  43148  mapfzcons1  43149  diophin  43204  iocunico  43639  rp-fakeuninass  43943  rclexi  44042  rtrclex  44044  dfrtrcl5  44056  dfrcl2  44101  corcltrcl  44166  cotrclrcl  44169  frege109d  44184  frege131d  44191  nregmodelf1o  45442  fiiuncl  45496  cnrefiisp  46258  fourierdlem65  46599  fourierdlem89  46623  fourierdlem90  46624  fourierdlem91  46625  fourierdlem96  46630  fourierdlem97  46631  fourierdlem98  46632  fourierdlem99  46633  fourierdlem100  46634  fourierdlem105  46639  fourierdlem108  46642  fourierdlem109  46643  fourierdlem110  46644  fourierdlem112  46646  fourierdlem113  46647  isomenndlem  46958  hoidmvlelem3  47025  1fzopredsuc  47773  dfclnbgr4  48300  clnbupgr  48309  usgrexmpl2edg  48505  lmod1zr  48969  dftpos5  49349  dftpos6  49350  tposresg  49353  tposrescnv  49354  tposres3  49356