Theorem uneq2i 4115

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

Syntax hints:   = wceq 1541   ∪ cun 3897

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 2115  ax-9 2123  ax-ext 2706

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 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-un 3904

This theorem is referenced by:  un4  4125  unundir  4127  difdif2  4246  difun2  4431  difdifdir  4442  dfif5  4494  qdass  4708  qdassr  4709  ssunpr  4788  iununi  5052  unidif0  5303  difxp1  6121  iunsuc  6402  fresaun  6703  fresaunres2  6704  fmptap  7114  fvsnun1  7126  funiunfv  7192  onuninsuci  7780  frrlem14  8239  tfrlem10  8316  oarec  8487  dfdom2  8913  fodomr  9054  fodomfir  9226  ranksuc  9775  kmlem3  10061  djuassen  10087  fin1a2lem10  10317  fin1a2lem12  10319  axdc3lem4  10361  prunioo  13395  fz0sn0fz1  13559  facnn  14196  fac0  14197  hashun3  14305  trclublem  14916  dmtrclfv  14939  fsum2dlem  15691  fsumiun  15742  incexclem  15757  fprod2dlem  15901  prmreclem4  16845  phlstr  17264  mreexexlem4d  17568  smndex1basss  18828  smndex1mgm  18830  opsrtoslem2  22009  restcld  23114  neitr  23122  fiuncmp  23346  refun0  23457  1stckgenlem  23495  filconn  23825  ufildr  23873  alexsubALTlem3  23991  ptcmplem1  23994  restmetu  24512  ovolfiniun  25456  unmbl  25492  volfiniun  25502  voliunlem1  25505  plyun0  26156  lgsquadlem3  27347  noextend  27632  noextendseq  27633  nosupbday  27671  nosupbnd1  27680  nosupbnd2  27682  noinfbday  27686  noinfbnd1  27695  noinfbnd2  27697  noetasuplem2  27700  noetasuplem3  27701  noetasuplem4  27702  noetainflem4  27706  madeun  27856  addsproplem2  27940  addsasslem1  27973  addsasslem2  27974  negsproplem2  27998  negsproplem6  28002  negsid  28010  mulsproplem2  28086  mulsproplem3  28087  mulsproplem4  28088  mulsproplem12  28096  mulsproplem13  28097  mulsproplem14  28098  mulsass  28135  precsexlemcbv  28174  onmulscl  28242  axlowdimlem3  28966  axlowdimlem17  28980  ex-un  30448  ex-pw  30453  indifundif  32548  iuninc  32584  difico  32812  esum2dlem  34198  fiunelcarsg  34422  carsgclctunlem1  34423  carsggect  34424  bnj601  35025  bnj1416  35144  subfacp1lem1  35322  cvmliftlem10  35437  satf0  35515  poimirlem4  37764  poimirlem18  37778  poimirlem21  37781  poimirlem22  37782  poimirlem25  37785  mbfresfi  37806  asindmre  37843  dmuncnvepres  38515  blockadjliftmap  38572  fsuppssind  42778  mapfzcons  42900  mapfzcons1  42901  diophin  42956  iocunico  43395  rp-fakeuninass  43699  rclexi  43798  rtrclex  43800  dfrtrcl5  43812  dfrcl2  43857  corcltrcl  43922  cotrclrcl  43925  frege109d  43940  frege131d  43947  nregmodelf1o  45198  fiiuncl  45252  cnrefiisp  46016  fourierdlem65  46357  fourierdlem89  46381  fourierdlem90  46382  fourierdlem91  46383  fourierdlem96  46388  fourierdlem97  46389  fourierdlem98  46390  fourierdlem99  46391  fourierdlem100  46392  fourierdlem105  46397  fourierdlem108  46400  fourierdlem109  46401  fourierdlem110  46402  fourierdlem112  46404  fourierdlem113  46405  isomenndlem  46716  hoidmvlelem3  46783  1fzopredsuc  47512  dfclnbgr4  48012  clnbupgr  48021  usgrexmpl2edg  48217  lmod1zr  48681  dftpos5  49061  dftpos6  49062  tposresg  49065  tposrescnv  49066  tposres3  49068