Theorem uneq2i 4119

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

Syntax hints:   = wceq 1542   ∪ cun 3901

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 3444  df-un 3908

This theorem is referenced by:  un4  4129  unundir  4131  difdif2  4250  difun2  4435  difdifdir  4446  dfif5  4498  qdass  4712  qdassr  4713  ssunpr  4792  iununi  5056  unidif0  5307  difxp1  6131  iunsuc  6412  fresaun  6713  fresaunres2  6714  fmptap  7126  fvsnun1  7138  funiunfv  7204  onuninsuci  7792  frrlem14  8251  tfrlem10  8328  oarec  8499  dfdom2  8927  fodomr  9068  fodomfir  9240  ranksuc  9789  kmlem3  10075  djuassen  10101  fin1a2lem10  10331  fin1a2lem12  10333  axdc3lem4  10375  prunioo  13409  fz0sn0fz1  13573  facnn  14210  fac0  14211  hashun3  14319  trclublem  14930  dmtrclfv  14953  fsum2dlem  15705  fsumiun  15756  incexclem  15771  fprod2dlem  15915  prmreclem4  16859  phlstr  17278  mreexexlem4d  17582  smndex1basss  18842  smndex1mgm  18844  opsrtoslem2  22023  restcld  23128  neitr  23136  fiuncmp  23360  refun0  23471  1stckgenlem  23509  filconn  23839  ufildr  23887  alexsubALTlem3  24005  ptcmplem1  24008  restmetu  24526  ovolfiniun  25470  unmbl  25506  volfiniun  25516  voliunlem1  25519  plyun0  26170  lgsquadlem3  27361  noextend  27646  noextendseq  27647  nosupbday  27685  nosupbnd1  27694  nosupbnd2  27696  noinfbday  27700  noinfbnd1  27709  noinfbnd2  27711  noetasuplem2  27714  noetasuplem3  27715  noetasuplem4  27716  noetainflem4  27720  madeun  27892  addsproplem2  27978  addsasslem1  28011  addsasslem2  28012  negsproplem2  28037  negsproplem6  28041  negsid  28049  mulsproplem2  28125  mulsproplem3  28126  mulsproplem4  28127  mulsproplem12  28135  mulsproplem13  28136  mulsproplem14  28137  mulsass  28174  precsexlemcbv  28214  onmulscl  28286  axlowdimlem3  29029  axlowdimlem17  29043  ex-un  30511  ex-pw  30516  indifundif  32611  iuninc  32647  difico  32874  esum2dlem  34270  fiunelcarsg  34494  carsgclctunlem1  34495  carsggect  34496  bnj601  35096  bnj1416  35215  subfacp1lem1  35395  cvmliftlem10  35510  satf0  35588  poimirlem4  37875  poimirlem18  37889  poimirlem21  37892  poimirlem22  37893  poimirlem25  37896  mbfresfi  37917  asindmre  37954  dmuncnvepres  38642  blockadjliftmap  38709  fsuppssind  42951  mapfzcons  43073  mapfzcons1  43074  diophin  43129  iocunico  43568  rp-fakeuninass  43872  rclexi  43971  rtrclex  43973  dfrtrcl5  43985  dfrcl2  44030  corcltrcl  44095  cotrclrcl  44098  frege109d  44113  frege131d  44120  nregmodelf1o  45371  fiiuncl  45425  cnrefiisp  46188  fourierdlem65  46529  fourierdlem89  46553  fourierdlem90  46554  fourierdlem91  46555  fourierdlem96  46560  fourierdlem97  46561  fourierdlem98  46562  fourierdlem99  46563  fourierdlem100  46564  fourierdlem105  46569  fourierdlem108  46572  fourierdlem109  46573  fourierdlem110  46574  fourierdlem112  46576  fourierdlem113  46577  isomenndlem  46888  hoidmvlelem3  46955  1fzopredsuc  47684  dfclnbgr4  48184  clnbupgr  48193  usgrexmpl2edg  48389  lmod1zr  48853  dftpos5  49233  dftpos6  49234  tposresg  49237  tposrescnv  49238  tposres3  49240