Theorem uneq2i 4117

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

Syntax hints:   = wceq 1541   ∪ cun 3899

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-un 3906

This theorem is referenced by:  un4  4127  unundir  4129  difdif2  4248  difun2  4433  difdifdir  4444  dfif5  4496  qdass  4710  qdassr  4711  ssunpr  4790  iununi  5054  unidif0  5305  difxp1  6123  iunsuc  6404  fresaun  6705  fresaunres2  6706  fmptap  7116  fvsnun1  7128  funiunfv  7194  onuninsuci  7782  frrlem14  8241  tfrlem10  8318  oarec  8489  dfdom2  8915  fodomr  9056  fodomfir  9228  ranksuc  9777  kmlem3  10063  djuassen  10089  fin1a2lem10  10319  fin1a2lem12  10321  axdc3lem4  10363  prunioo  13397  fz0sn0fz1  13561  facnn  14198  fac0  14199  hashun3  14307  trclublem  14918  dmtrclfv  14941  fsum2dlem  15693  fsumiun  15744  incexclem  15759  fprod2dlem  15903  prmreclem4  16847  phlstr  17266  mreexexlem4d  17570  smndex1basss  18830  smndex1mgm  18832  opsrtoslem2  22011  restcld  23116  neitr  23124  fiuncmp  23348  refun0  23459  1stckgenlem  23497  filconn  23827  ufildr  23875  alexsubALTlem3  23993  ptcmplem1  23996  restmetu  24514  ovolfiniun  25458  unmbl  25494  volfiniun  25504  voliunlem1  25507  plyun0  26158  lgsquadlem3  27349  noextend  27634  noextendseq  27635  nosupbday  27673  nosupbnd1  27682  nosupbnd2  27684  noinfbday  27688  noinfbnd1  27697  noinfbnd2  27699  noetasuplem2  27702  noetasuplem3  27703  noetasuplem4  27704  noetainflem4  27708  madeun  27880  addsproplem2  27966  addsasslem1  27999  addsasslem2  28000  negsproplem2  28025  negsproplem6  28029  negsid  28037  mulsproplem2  28113  mulsproplem3  28114  mulsproplem4  28115  mulsproplem12  28123  mulsproplem13  28124  mulsproplem14  28125  mulsass  28162  precsexlemcbv  28202  onmulscl  28274  axlowdimlem3  29017  axlowdimlem17  29031  ex-un  30499  ex-pw  30504  indifundif  32599  iuninc  32635  difico  32863  esum2dlem  34249  fiunelcarsg  34473  carsgclctunlem1  34474  carsggect  34475  bnj601  35076  bnj1416  35195  subfacp1lem1  35373  cvmliftlem10  35488  satf0  35566  poimirlem4  37825  poimirlem18  37839  poimirlem21  37842  poimirlem22  37843  poimirlem25  37846  mbfresfi  37867  asindmre  37904  dmuncnvepres  38576  blockadjliftmap  38633  fsuppssind  42836  mapfzcons  42958  mapfzcons1  42959  diophin  43014  iocunico  43453  rp-fakeuninass  43757  rclexi  43856  rtrclex  43858  dfrtrcl5  43870  dfrcl2  43915  corcltrcl  43980  cotrclrcl  43983  frege109d  43998  frege131d  44005  nregmodelf1o  45256  fiiuncl  45310  cnrefiisp  46074  fourierdlem65  46415  fourierdlem89  46439  fourierdlem90  46440  fourierdlem91  46441  fourierdlem96  46446  fourierdlem97  46447  fourierdlem98  46448  fourierdlem99  46449  fourierdlem100  46450  fourierdlem105  46455  fourierdlem108  46458  fourierdlem109  46459  fourierdlem110  46460  fourierdlem112  46462  fourierdlem113  46463  isomenndlem  46774  hoidmvlelem3  46841  1fzopredsuc  47570  dfclnbgr4  48070  clnbupgr  48079  usgrexmpl2edg  48275  lmod1zr  48739  dftpos5  49119  dftpos6  49120  tposresg  49123  tposrescnv  49124  tposres3  49126