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 2732

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 2739  df-cleq 2752  df-clel 2835  df-v 3452  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  5324  unidif0OLD  5325  difxp1  6157  iunsuc  6445  fresaun  6747  fresaunres2  6748  fmptap  7169  fvsnun1  7181  funiunfv  7246  onuninsuci  7837  frrlem14  8299  tfrlem10  8377  oarec  8550  dfdom2  8985  fodomr  9127  fodomfir  9298  ranksuc  9848  kmlem3  10156  djuassen  10182  fin1a2lem10  10412  fin1a2lem12  10414  axdc3lem4  10456  prunioo  13535  fz0sn0fz1  13701  facnn  14340  fac0  14341  hashun3  14449  trclublem  15069  dmtrclfv  15092  fsum2dlem  15857  fsumiun  15909  incexclem  15926  fprod2dlem  16068  prmreclem4  17012  phlstr  17432  mreexexlem4d  17736  smndex1basss  19018  smndex1mgm  19020  opsrtoslem2  22273  restcld  23398  neitr  23406  fiuncmp  23630  refun0  23742  1stckgenlem  23780  filconn  24110  ufildr  24158  alexsubALTlem3  24276  ptcmplem1  24279  restmetu  24797  ovolfiniun  25730  unmbl  25766  volfiniun  25776  voliunlem1  25779  plyun0  26423  lgsquadlem3  27619  noextend  27903  noextendseq  27904  nosupbday  27942  nosupbnd1  27951  nosupbnd2  27953  noinfbday  27957  noinfbnd1  27966  noinfbnd2  27968  noetasuplem2  27971  noetasuplem3  27972  noetasuplem4  27973  noetainflem4  27977  madeun  28150  addsproplem2  28236  addsasslem1  28269  addsasslem2  28270  negsproplem2  28295  negsproplem6  28299  negsid  28307  mulsproplem2  28383  mulsproplem3  28384  mulsproplem4  28385  mulsproplem12  28393  mulsproplem13  28394  mulsproplem14  28395  mulsass  28432  precsexlemcbv  28472  onmulscl  28544  axlowdimlem3  29402  axlowdimlem17  29416  ex-un  30905  ex-pw  30910  indifundif  33000  iuninc  33035  difico  33255  esum2dlem  34603  fiunelcarsg  34828  carsgclctunlem1  34829  carsggect  34830  bnj601  35430  bnj1416  35549  subfacp1lem1  35759  cvmliftlem10  35874  satf0  35952  poimirlem4  38374  poimirlem18  38388  poimirlem21  38391  poimirlem22  38392  poimirlem25  38395  mbfresfi  38416  asindmre  38453  dmuncnvepres  39140  blockadjliftmap  39207  fsuppssind  43440  mapfzcons  43562  mapfzcons1  43563  diophin  43618  iocunico  44053  rp-fakeuninass  44357  rclexi  44456  rtrclex  44458  dfrtrcl5  44470  dfrcl2  44515  corcltrcl  44580  cotrclrcl  44583  frege109d  44598  frege131d  44605  nregmodelf1o  45839  fiiuncl  45900  cnrefiisp  46659  fourierdlem65  47000  fourierdlem89  47024  fourierdlem90  47025  fourierdlem91  47026  fourierdlem96  47031  fourierdlem97  47032  fourierdlem98  47033  fourierdlem99  47034  fourierdlem100  47035  fourierdlem105  47040  fourierdlem108  47043  fourierdlem109  47044  fourierdlem110  47045  fourierdlem112  47047  fourierdlem113  47048  isomenndlem  47359  hoidmvlelem3  47426  1fzopredsuc  48214  dfclnbgr4  48741  clnbupgr  48750  usgrexmpl2edg  48946  lmod1zr  49424  dftpos5  49801  dftpos6  49802  tposresg  49805  tposrescnv  49806  tposres3  49808