Theorem uneq2i 4119

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

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

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 2148  ax-9 2156  ax-ext 2737

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 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3911

This theorem is used by:  un4  4128  unundir  4130  difdif2  4249  difun2  4444  difdifdir  4454  dfif5  4506  qdass  4721  qdassr  4722  ssunpr  4801  iununi  5067  unidif0  5332  unidif0OLD  5333  difxp1  6164  iunsuc  6452  fresaun  6753  fresaunres2  6754  fmptap  7174  fvsnun1  7186  funiunfv  7251  onuninsuci  7842  frrlem14  8302  tfrlem10  8380  oarec  8553  dfdom2  8981  fodomr  9123  fodomfir  9294  ranksuc  9844  kmlem3  10152  djuassen  10178  fin1a2lem10  10408  fin1a2lem12  10410  axdc3lem4  10452  prunioo  13524  fz0sn0fz1  13690  facnn  14329  fac0  14330  hashun3  14438  trclublem  15056  dmtrclfv  15079  fsum2dlem  15844  fsumiun  15896  incexclem  15913  fprod2dlem  16057  prmreclem4  17001  phlstr  17421  mreexexlem4d  17725  smndex1basss  19004  smndex1mgm  19006  opsrtoslem2  22257  restcld  23379  neitr  23387  fiuncmp  23611  refun0  23723  1stckgenlem  23761  filconn  24091  ufildr  24139  alexsubALTlem3  24257  ptcmplem1  24260  restmetu  24778  ovolfiniun  25711  unmbl  25747  volfiniun  25757  voliunlem1  25760  plyun0  26405  lgsquadlem3  27597  noextend  27881  noextendseq  27882  nosupbday  27920  nosupbnd1  27929  nosupbnd2  27931  noinfbday  27935  noinfbnd1  27944  noinfbnd2  27946  noetasuplem2  27949  noetasuplem3  27950  noetasuplem4  27951  noetainflem4  27955  madeun  28128  addsproplem2  28214  addsasslem1  28247  addsasslem2  28248  negsproplem2  28273  negsproplem6  28277  negsid  28285  mulsproplem2  28361  mulsproplem3  28362  mulsproplem4  28363  mulsproplem12  28371  mulsproplem13  28372  mulsproplem14  28373  mulsass  28410  precsexlemcbv  28450  onmulscl  28522  axlowdimlem3  29349  axlowdimlem17  29363  ex-un  30846  ex-pw  30851  indifundif  32941  iuninc  32976  difico  33198  esum2dlem  34546  fiunelcarsg  34771  carsgclctunlem1  34772  carsggect  34773  bnj601  35373  bnj1416  35492  subfacp1lem1  35708  cvmliftlem10  35823  satf0  35901  poimirlem4  38332  poimirlem18  38346  poimirlem21  38349  poimirlem22  38350  poimirlem25  38353  mbfresfi  38374  asindmre  38411  dmuncnvepres  39098  blockadjliftmap  39165  fsuppssind  43383  mapfzcons  43505  mapfzcons1  43506  diophin  43561  iocunico  43996  rp-fakeuninass  44300  rclexi  44399  rtrclex  44401  dfrtrcl5  44413  dfrcl2  44458  corcltrcl  44523  cotrclrcl  44526  frege109d  44541  frege131d  44548  nregmodelf1o  45782  fiiuncl  45843  cnrefiisp  46602  fourierdlem65  46943  fourierdlem89  46967  fourierdlem90  46968  fourierdlem91  46969  fourierdlem96  46974  fourierdlem97  46975  fourierdlem98  46976  fourierdlem99  46977  fourierdlem100  46978  fourierdlem105  46983  fourierdlem108  46986  fourierdlem109  46987  fourierdlem110  46988  fourierdlem112  46990  fourierdlem113  46991  isomenndlem  47302  hoidmvlelem3  47369  1fzopredsuc  48120  dfclnbgr4  48647  clnbupgr  48656  usgrexmpl2edg  48852  lmod1zr  49330  dftpos5  49709  dftpos6  49710  tposresg  49713  tposrescnv  49714  tposres3  49716