Theorem uneq2i 4118

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

Syntax hints:   = wceq 1560   ∪ cun 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-un 3909

This theorem is referenced by:  un4  4127  unundir  4129  difdif2  4248  difun2  4435  difdifdir  4445  dfif5  4497  qdass  4712  qdassr  4713  ssunpr  4792  iununi  5056  unidif0  5316  unidif0OLD  5317  difxp1  6150  iunsuc  6433  fresaun  6735  fresaunres2  6736  fmptap  7154  fvsnun1  7166  funiunfv  7232  onuninsuci  7820  frrlem14  8280  tfrlem10  8358  oarec  8531  dfdom2  8959  fodomr  9100  fodomfir  9272  ranksuc  9823  kmlem3  10109  djuassen  10135  fin1a2lem10  10366  fin1a2lem12  10368  axdc3lem4  10410  prunioo  13485  fz0sn0fz1  13650  facnn  14288  fac0  14289  hashun3  14397  trclublem  15008  dmtrclfv  15031  fsum2dlem  15797  fsumiun  15849  incexclem  15866  fprod2dlem  16010  prmreclem4  16955  phlstr  17375  mreexexlem4d  17679  smndex1basss  18942  smndex1mgm  18944  opsrtoslem2  22109  restcld  23232  neitr  23240  fiuncmp  23464  refun0  23575  1stckgenlem  23613  filconn  23943  ufildr  23991  alexsubALTlem3  24109  ptcmplem1  24112  restmetu  24630  ovolfiniun  25563  unmbl  25599  volfiniun  25609  voliunlem1  25612  plyun0  26257  lgsquadlem3  27446  noextend  27730  noextendseq  27731  nosupbday  27769  nosupbnd1  27778  nosupbnd2  27780  noinfbday  27784  noinfbnd1  27793  noinfbnd2  27795  noetasuplem2  27798  noetasuplem3  27799  noetasuplem4  27800  noetainflem4  27804  madeun  27977  addsproplem2  28063  addsasslem1  28096  addsasslem2  28097  negsproplem2  28122  negsproplem6  28126  negsid  28134  mulsproplem2  28210  mulsproplem3  28211  mulsproplem4  28212  mulsproplem12  28220  mulsproplem13  28221  mulsproplem14  28222  mulsass  28259  precsexlemcbv  28299  onmulscl  28371  axlowdimlem3  29145  axlowdimlem17  29159  ex-un  30626  ex-pw  30631  indifundif  32723  iuninc  32760  difico  32985  esum2dlem  34389  fiunelcarsg  34613  carsgclctunlem1  34614  carsggect  34615  bnj601  35215  bnj1416  35334  subfacp1lem1  35529  cvmliftlem10  35644  satf0  35722  poimirlem4  38123  poimirlem18  38137  poimirlem21  38140  poimirlem22  38141  poimirlem25  38144  mbfresfi  38165  asindmre  38202  dmuncnvepres  38890  blockadjliftmap  38957  fsuppssind  43175  mapfzcons  43297  mapfzcons1  43298  diophin  43353  iocunico  43788  rp-fakeuninass  44092  rclexi  44191  rtrclex  44193  dfrtrcl5  44205  dfrcl2  44250  corcltrcl  44315  cotrclrcl  44318  frege109d  44333  frege131d  44340  nregmodelf1o  45591  fiiuncl  45645  cnrefiisp  46404  fourierdlem65  46745  fourierdlem89  46769  fourierdlem90  46770  fourierdlem91  46771  fourierdlem96  46776  fourierdlem97  46777  fourierdlem98  46778  fourierdlem99  46779  fourierdlem100  46780  fourierdlem105  46785  fourierdlem108  46788  fourierdlem109  46789  fourierdlem110  46790  fourierdlem112  46792  fourierdlem113  46793  isomenndlem  47104  hoidmvlelem3  47171  1fzopredsuc  47919  dfclnbgr4  48446  clnbupgr  48455  usgrexmpl2edg  48651  lmod1zr  49115  dftpos5  49495  dftpos6  49496  tposresg  49499  tposrescnv  49500  tposres3  49502