Theorem uneq2i 4095

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

Syntax hints:   = wceq 1547   ∪ cun 3881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-un 3888

This theorem is referenced by:  un4  4104  unundir  4106  difdif2  4224  difun2  4409  difdifdir  4419  dfif5  4471  qdass  4685  qdassr  4686  ssunpr  4765  iununi  5028  unidif0  5288  unidif0OLD  5289  difxp1  6116  iunsuc  6397  fresaun  6698  fresaunres2  6699  fmptap  7114  fvsnun1  7126  funiunfv  7192  onuninsuci  7780  frrlem14  8239  tfrlem10  8316  oarec  8487  dfdom2  8915  fodomr  9056  fodomfir  9228  ranksuc  9780  kmlem3  10066  djuassen  10092  fin1a2lem10  10322  fin1a2lem12  10324  axdc3lem4  10366  prunioo  13425  fz0sn0fz1  13590  facnn  14228  fac0  14229  hashun3  14337  trclublem  14948  dmtrclfv  14971  fsum2dlem  15723  fsumiun  15775  incexclem  15792  fprod2dlem  15936  prmreclem4  16881  phlstr  17300  mreexexlem4d  17604  smndex1basss  18867  smndex1mgm  18869  opsrtoslem2  22032  restcld  23155  neitr  23163  fiuncmp  23387  refun0  23498  1stckgenlem  23536  filconn  23866  ufildr  23914  alexsubALTlem3  24032  ptcmplem1  24035  restmetu  24553  ovolfiniun  25486  unmbl  25522  volfiniun  25532  voliunlem1  25535  plyun0  26180  lgsquadlem3  27363  noextend  27648  noextendseq  27649  nosupbday  27687  nosupbnd1  27696  nosupbnd2  27698  noinfbday  27702  noinfbnd1  27711  noinfbnd2  27713  noetasuplem2  27716  noetasuplem3  27717  noetasuplem4  27718  noetainflem4  27722  madeun  27894  addsproplem2  27980  addsasslem1  28013  addsasslem2  28014  negsproplem2  28039  negsproplem6  28043  negsid  28051  mulsproplem2  28127  mulsproplem3  28128  mulsproplem4  28129  mulsproplem12  28137  mulsproplem13  28138  mulsproplem14  28139  mulsass  28176  precsexlemcbv  28216  onmulscl  28288  axlowdimlem3  29031  axlowdimlem17  29045  ex-un  30512  ex-pw  30517  indifundif  32612  iuninc  32649  difico  32875  esum2dlem  34276  fiunelcarsg  34500  carsgclctunlem1  34501  carsggect  34502  bnj601  35102  bnj1416  35221  subfacp1lem1  35407  cvmliftlem10  35522  satf0  35600  poimirlem4  37991  poimirlem18  38005  poimirlem21  38008  poimirlem22  38009  poimirlem25  38012  mbfresfi  38033  asindmre  38070  dmuncnvepres  38758  blockadjliftmap  38825  fsuppssind  43043  mapfzcons  43165  mapfzcons1  43166  diophin  43221  iocunico  43656  rp-fakeuninass  43960  rclexi  44059  rtrclex  44061  dfrtrcl5  44073  dfrcl2  44118  corcltrcl  44183  cotrclrcl  44186  frege109d  44201  frege131d  44208  nregmodelf1o  45459  fiiuncl  45513  cnrefiisp  46273  fourierdlem65  46614  fourierdlem89  46638  fourierdlem90  46639  fourierdlem91  46640  fourierdlem96  46645  fourierdlem97  46646  fourierdlem98  46647  fourierdlem99  46648  fourierdlem100  46649  fourierdlem105  46654  fourierdlem108  46657  fourierdlem109  46658  fourierdlem110  46659  fourierdlem112  46661  fourierdlem113  46662  isomenndlem  46973  hoidmvlelem3  47040  1fzopredsuc  47788  dfclnbgr4  48315  clnbupgr  48324  usgrexmpl2edg  48520  lmod1zr  48984  dftpos5  49364  dftpos6  49365  tposresg  49368  tposrescnv  49369  tposres3  49371