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 ⊢ (𝐶 ∪ 𝐴) = (𝐶 ∪ 𝐵)

This proof depends on syntax axioms:   = wceq 1570   ∪ cun 3897

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-un 3904

This theorem is used by:  un4  4121  unundir  4123  difdif2  4242  difun2  4437  difdifdir  4447  dfif5  4499  qdass  4714  qdassr  4715  ssunpr  4794  iununi  5059  unidif0  5321  unidif0OLD  5322  difxp1  6156  iunsuc  6450  fresaun  6753  fresaunres2  6754  fmptap  7175  fvsnun1  7187  funiunfv  7252  onuninsuci  7851  frrlem14  8317  tfrlem10  8395  oarec  8570  dfdom2  9005  fodomr  9147  fodomfir  9319  ranksuc  9882  kmlem3  10231  djuassen  10257  fin1a2lem10  10487  fin1a2lem12  10489  axdc3lem4  10531  prunioo  13612  fz0sn0fz1  13779  facnn  14419  fac0  14420  hashun3  14528  trclublem  15148  dmtrclfv  15171  fsum2dlem  15936  fsumiun  15988  incexclem  16005  fprod2dlem  16147  prmreclem4  17097  phlstr  17517  mreexexlem4d  17821  smndex1basss  19104  smndex1mgm  19106  opsrtoslem2  22365  restcld  23490  neitr  23498  fiuncmp  23722  refun0  23834  1stckgenlem  23872  filconn  24202  ufildr  24250  alexsubALTlem3  24368  ptcmplem1  24371  restmetu  24889  ovolfiniun  25822  unmbl  25858  volfiniun  25868  voliunlem1  25871  plyun0  26515  lgsquadlem3  27709  noextend  28023  noextendseq  28024  nosupbday  28062  nosupbnd1  28071  nosupbnd2  28073  noinfbday  28077  noinfbnd1  28086  noinfbnd2  28088  noetasuplem2  28091  noetasuplem3  28092  noetasuplem4  28093  noetainflem4  28097  madeun  28270  addsproplem2  28356  addsasslem1  28389  addsasslem2  28390  negsproplem2  28415  negsproplem6  28419  negsid  28427  mulsproplem2  28503  mulsproplem3  28504  mulsproplem4  28505  mulsproplem12  28513  mulsproplem13  28514  mulsproplem14  28515  mulsass  28552  precsexlemcbv  28592  onmulscl  28664  axlowdimlem3  29522  axlowdimlem17  29536  ex-un  31025  ex-pw  31030  indifundif  33120  iuninc  33155  difico  33375  esum2dlem  34724  fiunelcarsg  34948  carsgclctunlem1  34949  carsggect  34950  bnj601  35550  bnj1416  35669  subfacp1lem1  35944  cvmliftlem10  36059  satf0  36137  poimirlem4  38542  poimirlem18  38556  poimirlem21  38559  poimirlem22  38560  poimirlem25  38563  mbfresfi  38584  asindmre  38621  dmuncnvepres  39323  blockadjliftmap  39390  fsuppssind  43621  mapfzcons  43726  mapfzcons1  43727  diophin  43782  iocunico  44212  rp-fakeuninass  44516  rclexi  44614  rtrclex  44616  dfrtrcl5  44628  dfrcl2  44673  corcltrcl  44738  cotrclrcl  44741  frege109d  44756  frege131d  44763  nregmodelf1o  46004  fiiuncl  46081  cnrefiisp  46839  fourierdlem65  47180  fourierdlem89  47204  fourierdlem90  47205  fourierdlem91  47206  fourierdlem96  47211  fourierdlem97  47212  fourierdlem98  47213  fourierdlem99  47214  fourierdlem100  47215  fourierdlem105  47220  fourierdlem108  47223  fourierdlem109  47224  fourierdlem110  47225  fourierdlem112  47227  fourierdlem113  47228  isomenndlem  47539  hoidmvlelem3  47606  1fzopredsuc  48394  dfclnbgr4  48921  clnbupgr  48930  usgrexmpl2edg  49126  lmod1zr  49604  dftpos5  49981  dftpos6  49982  tposresg  49985  tposrescnv  49986  tposres3  49988