Theorem uneq2i 4112

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

Syntax hints:   = wceq 1541   ∪ cun 3895

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-un 3902

This theorem is referenced by:  un4  4122  unundir  4124  difdif2  4243  difun2  4428  difdifdir  4439  dfif5  4489  qdass  4703  qdassr  4704  ssunpr  4783  iununi  5045  unidif0  5296  difxp1  6112  iunsuc  6393  fresaun  6694  fresaunres2  6695  fmptap  7104  fvsnun1  7116  funiunfv  7182  onuninsuci  7770  frrlem14  8229  tfrlem10  8306  oarec  8477  dfdom2  8900  fodomr  9041  fodomfir  9212  ranksuc  9758  kmlem3  10044  djuassen  10070  fin1a2lem10  10300  fin1a2lem12  10302  axdc3lem4  10344  prunioo  13381  fz0sn0fz1  13545  facnn  14182  fac0  14183  hashun3  14291  trclublem  14902  dmtrclfv  14925  fsum2dlem  15677  fsumiun  15728  incexclem  15743  fprod2dlem  15887  prmreclem4  16831  phlstr  17250  mreexexlem4d  17553  smndex1basss  18813  smndex1mgm  18815  opsrtoslem2  21991  restcld  23087  neitr  23095  fiuncmp  23319  refun0  23430  1stckgenlem  23468  filconn  23798  ufildr  23846  alexsubALTlem3  23964  ptcmplem1  23967  restmetu  24485  ovolfiniun  25429  unmbl  25465  volfiniun  25475  voliunlem1  25478  plyun0  26129  lgsquadlem3  27320  noextend  27605  noextendseq  27606  nosupbday  27644  nosupbnd1  27653  nosupbnd2  27655  noinfbday  27659  noinfbnd1  27668  noinfbnd2  27670  noetasuplem2  27673  noetasuplem3  27674  noetasuplem4  27675  noetainflem4  27679  madeun  27829  addsproplem2  27913  addsasslem1  27946  addsasslem2  27947  negsproplem2  27971  negsproplem6  27975  negsid  27983  mulsproplem2  28056  mulsproplem3  28057  mulsproplem4  28058  mulsproplem12  28066  mulsproplem13  28067  mulsproplem14  28068  mulsass  28105  precsexlemcbv  28144  onmulscl  28211  axlowdimlem3  28922  axlowdimlem17  28936  ex-un  30404  ex-pw  30409  indifundif  32504  iuninc  32540  difico  32766  esum2dlem  34105  fiunelcarsg  34329  carsgclctunlem1  34330  carsggect  34331  bnj601  34932  bnj1416  35051  subfacp1lem1  35223  cvmliftlem10  35338  satf0  35416  poimirlem4  37674  poimirlem18  37688  poimirlem21  37691  poimirlem22  37692  poimirlem25  37695  mbfresfi  37716  asindmre  37753  dmuncnvepres  38425  blockadjliftmap  38482  fsuppssind  42696  mapfzcons  42819  mapfzcons1  42820  diophin  42875  iocunico  43314  rp-fakeuninass  43619  rclexi  43718  rtrclex  43720  dfrtrcl5  43732  dfrcl2  43777  corcltrcl  43842  cotrclrcl  43845  frege109d  43860  frege131d  43867  nregmodelf1o  45118  fiiuncl  45172  cnrefiisp  45938  fourierdlem65  46279  fourierdlem89  46303  fourierdlem90  46304  fourierdlem91  46305  fourierdlem96  46310  fourierdlem97  46311  fourierdlem98  46312  fourierdlem99  46313  fourierdlem100  46314  fourierdlem105  46319  fourierdlem108  46322  fourierdlem109  46323  fourierdlem110  46324  fourierdlem112  46326  fourierdlem113  46327  isomenndlem  46638  hoidmvlelem3  46705  1fzopredsuc  47434  dfclnbgr4  47934  clnbupgr  47943  usgrexmpl2edg  48139  lmod1zr  48604  dftpos5  48984  dftpos6  48985  tposresg  48988  tposrescnv  48989  tposres3  48991