Theorem uneq2i 4128

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

Syntax hints:   = wceq 1540   ∪ cun 3912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-un 3919

This theorem is referenced by:  un4  4138  unundir  4140  difdif2  4259  difun2  4444  difdifdir  4455  dfif5  4505  qdass  4717  qdassr  4718  ssunpr  4798  iununi  5063  unidif0  5315  difxp1  6138  iunsuc  6419  fresaun  6731  fresaunres2  6732  fvssunirnOLD  6892  fmptap  7144  fvsnun1  7156  funiunfv  7222  onuninsuci  7816  frrlem14  8278  tfrlem10  8355  oarec  8526  dfdom2  8949  fodomr  9092  fodomfir  9279  ranksuc  9818  kmlem3  10106  djuassen  10132  fin1a2lem10  10362  fin1a2lem12  10364  axdc3lem4  10406  prunioo  13442  fz0sn0fz1  13606  facnn  14240  fac0  14241  hashun3  14349  trclublem  14961  dmtrclfv  14984  fsum2dlem  15736  fsumiun  15787  incexclem  15802  fprod2dlem  15946  prmreclem4  16890  phlstr  17309  mreexexlem4d  17608  smndex1basss  18832  smndex1mgm  18834  opsrtoslem2  21963  restcld  23059  neitr  23067  fiuncmp  23291  refun0  23402  1stckgenlem  23440  filconn  23770  ufildr  23818  alexsubALTlem3  23936  ptcmplem1  23939  restmetu  24458  ovolfiniun  25402  unmbl  25438  volfiniun  25448  voliunlem1  25451  plyun0  26102  lgsquadlem3  27293  noextend  27578  noextendseq  27579  nosupbday  27617  nosupbnd1  27626  nosupbnd2  27628  noinfbday  27632  noinfbnd1  27641  noinfbnd2  27643  noetasuplem2  27646  noetasuplem3  27647  noetasuplem4  27648  noetainflem4  27652  madeun  27795  addsproplem2  27877  addsasslem1  27910  addsasslem2  27911  negsproplem2  27935  negsproplem6  27939  negsid  27947  mulsproplem2  28020  mulsproplem3  28021  mulsproplem4  28022  mulsproplem12  28030  mulsproplem13  28031  mulsproplem14  28032  mulsass  28069  precsexlemcbv  28108  onmulscl  28175  axlowdimlem3  28871  axlowdimlem17  28885  ex-un  30353  ex-pw  30358  indifundif  32453  iuninc  32489  difico  32706  esum2dlem  34082  fiunelcarsg  34307  carsgclctunlem1  34308  carsggect  34309  bnj601  34910  bnj1416  35029  subfacp1lem1  35166  cvmliftlem10  35281  satf0  35359  poimirlem4  37618  poimirlem18  37632  poimirlem21  37635  poimirlem22  37636  poimirlem25  37639  mbfresfi  37660  asindmre  37697  fsuppssind  42581  mapfzcons  42704  mapfzcons1  42705  diophin  42760  iocunico  43200  rp-fakeuninass  43505  rclexi  43604  rtrclex  43606  dfrtrcl5  43618  dfrcl2  43663  corcltrcl  43728  cotrclrcl  43731  frege109d  43746  frege131d  43753  nregmodelf1o  45005  fiiuncl  45059  cnrefiisp  45828  fourierdlem65  46169  fourierdlem89  46193  fourierdlem90  46194  fourierdlem91  46195  fourierdlem96  46200  fourierdlem97  46201  fourierdlem98  46202  fourierdlem99  46203  fourierdlem100  46204  fourierdlem105  46209  fourierdlem108  46212  fourierdlem109  46213  fourierdlem110  46214  fourierdlem112  46216  fourierdlem113  46217  isomenndlem  46528  hoidmvlelem3  46595  1fzopredsuc  47325  dfclnbgr4  47825  clnbupgr  47834  usgrexmpl2edg  48020  lmod1zr  48482  dftpos5  48862  dftpos6  48863  tposresg  48866  tposrescnv  48867  tposres3  48869