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  5298  difxp1  6124  iunsuc  6405  fresaun  6706  fresaunres2  6707  fmptap  7119  fvsnun1  7131  funiunfv  7197  onuninsuci  7785  frrlem14  8243  tfrlem10  8320  oarec  8491  dfdom2  8919  fodomr  9060  fodomfir  9232  ranksuc  9783  kmlem3  10069  djuassen  10095  fin1a2lem10  10325  fin1a2lem12  10327  axdc3lem4  10369  prunioo  13428  fz0sn0fz1  13593  facnn  14231  fac0  14232  hashun3  14340  trclublem  14951  dmtrclfv  14974  fsum2dlem  15726  fsumiun  15778  incexclem  15795  fprod2dlem  15939  prmreclem4  16884  phlstr  17303  mreexexlem4d  17607  smndex1basss  18870  smndex1mgm  18872  opsrtoslem2  22047  restcld  23150  neitr  23158  fiuncmp  23382  refun0  23493  1stckgenlem  23531  filconn  23861  ufildr  23909  alexsubALTlem3  24027  ptcmplem1  24030  restmetu  24548  ovolfiniun  25481  unmbl  25517  volfiniun  25527  voliunlem1  25530  plyun0  26175  lgsquadlem3  27362  noextend  27647  noextendseq  27648  nosupbday  27686  nosupbnd1  27695  nosupbnd2  27697  noinfbday  27701  noinfbnd1  27710  noinfbnd2  27712  noetasuplem2  27715  noetasuplem3  27716  noetasuplem4  27717  noetainflem4  27721  madeun  27893  addsproplem2  27979  addsasslem1  28012  addsasslem2  28013  negsproplem2  28038  negsproplem6  28042  negsid  28050  mulsproplem2  28126  mulsproplem3  28127  mulsproplem4  28128  mulsproplem12  28136  mulsproplem13  28137  mulsproplem14  28138  mulsass  28175  precsexlemcbv  28215  onmulscl  28287  axlowdimlem3  29030  axlowdimlem17  29044  ex-un  30512  ex-pw  30517  indifundif  32612  iuninc  32648  difico  32874  esum2dlem  34255  fiunelcarsg  34479  carsgclctunlem1  34480  carsggect  34481  bnj601  35081  bnj1416  35200  subfacp1lem1  35380  cvmliftlem10  35495  satf0  35573  poimirlem4  37962  poimirlem18  37976  poimirlem21  37979  poimirlem22  37980  poimirlem25  37983  mbfresfi  38004  asindmre  38041  dmuncnvepres  38729  blockadjliftmap  38796  fsuppssind  43043  mapfzcons  43165  mapfzcons1  43166  diophin  43221  iocunico  43660  rp-fakeuninass  43964  rclexi  44063  rtrclex  44065  dfrtrcl5  44077  dfrcl2  44122  corcltrcl  44187  cotrclrcl  44190  frege109d  44205  frege131d  44212  nregmodelf1o  45463  fiiuncl  45517  cnrefiisp  46279  fourierdlem65  46620  fourierdlem89  46644  fourierdlem90  46645  fourierdlem91  46646  fourierdlem96  46651  fourierdlem97  46652  fourierdlem98  46653  fourierdlem99  46654  fourierdlem100  46655  fourierdlem105  46660  fourierdlem108  46663  fourierdlem109  46664  fourierdlem110  46665  fourierdlem112  46667  fourierdlem113  46668  isomenndlem  46979  hoidmvlelem3  47046  1fzopredsuc  47788  dfclnbgr4  48315  clnbupgr  48324  usgrexmpl2edg  48520  lmod1zr  48984  dftpos5  49364  dftpos6  49365  tposresg  49368  tposrescnv  49369  tposres3  49371