Theorem uneq2i 4188

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

Syntax hints:   = wceq 1537   ∪ cun 3974

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-un 3981

This theorem is referenced by:  un4  4198  unundir  4200  difdif2  4315  difun2  4504  difdifdir  4515  dfif5  4564  qdass  4778  qdassr  4779  ssunpr  4859  iununi  5122  unidif0  5378  difxp1  6196  iunsuc  6480  fresaun  6792  fresaunres2  6793  fvssunirnOLD  6954  fmptap  7204  fvsnun1  7216  funiunfv  7285  onuninsuci  7877  frrlem14  8340  wfrlem13OLD  8377  wfrlem14OLD  8378  wfrlem16OLD  8380  tfrlem10  8443  oarec  8618  dfdom2  9038  fodomr  9194  fodomfir  9396  ranksuc  9934  kmlem3  10222  djuassen  10248  fin1a2lem10  10478  fin1a2lem12  10480  axdc3lem4  10522  prunioo  13541  fz0sn0fz1  13702  facnn  14324  fac0  14325  hashun3  14433  trclublem  15044  dmtrclfv  15067  fsum2dlem  15818  fsumiun  15869  incexclem  15884  fprod2dlem  16028  prmreclem4  16966  phlstr  17405  mreexexlem4d  17705  smndex1basss  18940  smndex1mgm  18942  opsrtoslem2  22103  restcld  23201  neitr  23209  fiuncmp  23433  refun0  23544  1stckgenlem  23582  filconn  23912  ufildr  23960  alexsubALTlem3  24078  ptcmplem1  24081  restmetu  24604  ovolfiniun  25555  unmbl  25591  volfiniun  25601  voliunlem1  25604  plyun0  26256  lgsquadlem3  27444  noextend  27729  noextendseq  27730  nosupbday  27768  nosupbnd1  27777  nosupbnd2  27779  noinfbday  27783  noinfbnd1  27792  noinfbnd2  27794  noetasuplem2  27797  noetasuplem3  27798  noetasuplem4  27799  noetainflem4  27803  madeun  27940  addsproplem2  28021  addsasslem1  28054  addsasslem2  28055  negsproplem2  28079  negsproplem6  28083  negsid  28091  mulsproplem2  28161  mulsproplem3  28162  mulsproplem4  28163  mulsproplem12  28171  mulsproplem13  28172  mulsproplem14  28173  mulsass  28210  precsexlemcbv  28248  onmulscl  28305  axlowdimlem3  28977  axlowdimlem17  28991  ex-un  30456  ex-pw  30461  indifundif  32554  iuninc  32583  difico  32788  esum2dlem  34056  fiunelcarsg  34281  carsgclctunlem1  34282  carsggect  34283  bnj601  34896  bnj1416  35015  subfacp1lem1  35147  cvmliftlem10  35262  satf0  35340  poimirlem4  37584  poimirlem18  37598  poimirlem21  37601  poimirlem22  37602  poimirlem25  37605  mbfresfi  37626  asindmre  37663  fsuppssind  42548  mapfzcons  42672  mapfzcons1  42673  diophin  42728  iocunico  43172  rp-fakeuninass  43478  rclexi  43577  rtrclex  43579  dfrtrcl5  43591  dfrcl2  43636  corcltrcl  43701  cotrclrcl  43704  frege109d  43719  frege131d  43726  fiiuncl  44967  cnrefiisp  45751  fourierdlem65  46092  fourierdlem89  46116  fourierdlem90  46117  fourierdlem91  46118  fourierdlem96  46123  fourierdlem97  46124  fourierdlem98  46125  fourierdlem99  46126  fourierdlem100  46127  fourierdlem105  46132  fourierdlem108  46135  fourierdlem109  46136  fourierdlem110  46137  fourierdlem112  46139  fourierdlem113  46140  isomenndlem  46451  hoidmvlelem3  46518  1fzopredsuc  47239  dfclnbgr4  47698  clnbupgr  47706  usgrexmpl2edg  47844  lmod1zr  48222