Theorem uneq2i 4164

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

Syntax hints:   = wceq 1539   ∪ cun 3948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-v 3481  df-un 3955

This theorem is referenced by:  un4  4174  unundir  4176  difdif2  4295  difun2  4480  difdifdir  4491  dfif5  4541  qdass  4752  qdassr  4753  ssunpr  4833  iununi  5098  unidif0  5359  difxp1  6184  iunsuc  6468  fresaun  6778  fresaunres2  6779  fvssunirnOLD  6939  fmptap  7191  fvsnun1  7203  funiunfv  7269  onuninsuci  7862  frrlem14  8325  wfrlem13OLD  8362  wfrlem14OLD  8363  wfrlem16OLD  8365  tfrlem10  8428  oarec  8601  dfdom2  9019  fodomr  9169  fodomfir  9369  ranksuc  9906  kmlem3  10194  djuassen  10220  fin1a2lem10  10450  fin1a2lem12  10452  axdc3lem4  10494  prunioo  13522  fz0sn0fz1  13686  facnn  14315  fac0  14316  hashun3  14424  trclublem  15035  dmtrclfv  15058  fsum2dlem  15807  fsumiun  15858  incexclem  15873  fprod2dlem  16017  prmreclem4  16958  phlstr  17391  mreexexlem4d  17691  smndex1basss  18919  smndex1mgm  18921  opsrtoslem2  22081  restcld  23181  neitr  23189  fiuncmp  23413  refun0  23524  1stckgenlem  23562  filconn  23892  ufildr  23940  alexsubALTlem3  24058  ptcmplem1  24061  restmetu  24584  ovolfiniun  25537  unmbl  25573  volfiniun  25583  voliunlem1  25586  plyun0  26237  lgsquadlem3  27427  noextend  27712  noextendseq  27713  nosupbday  27751  nosupbnd1  27760  nosupbnd2  27762  noinfbday  27766  noinfbnd1  27775  noinfbnd2  27777  noetasuplem2  27780  noetasuplem3  27781  noetasuplem4  27782  noetainflem4  27786  madeun  27923  addsproplem2  28004  addsasslem1  28037  addsasslem2  28038  negsproplem2  28062  negsproplem6  28066  negsid  28074  mulsproplem2  28144  mulsproplem3  28145  mulsproplem4  28146  mulsproplem12  28154  mulsproplem13  28155  mulsproplem14  28156  mulsass  28193  precsexlemcbv  28231  onmulscl  28288  axlowdimlem3  28960  axlowdimlem17  28974  ex-un  30444  ex-pw  30449  indifundif  32544  iuninc  32574  difico  32786  esum2dlem  34094  fiunelcarsg  34319  carsgclctunlem1  34320  carsggect  34321  bnj601  34935  bnj1416  35054  subfacp1lem1  35185  cvmliftlem10  35300  satf0  35378  poimirlem4  37632  poimirlem18  37646  poimirlem21  37649  poimirlem22  37650  poimirlem25  37653  mbfresfi  37674  asindmre  37711  fsuppssind  42608  mapfzcons  42732  mapfzcons1  42733  diophin  42788  iocunico  43228  rp-fakeuninass  43534  rclexi  43633  rtrclex  43635  dfrtrcl5  43647  dfrcl2  43692  corcltrcl  43757  cotrclrcl  43760  frege109d  43775  frege131d  43782  fiiuncl  45075  cnrefiisp  45850  fourierdlem65  46191  fourierdlem89  46215  fourierdlem90  46216  fourierdlem91  46217  fourierdlem96  46222  fourierdlem97  46223  fourierdlem98  46224  fourierdlem99  46225  fourierdlem100  46226  fourierdlem105  46231  fourierdlem108  46234  fourierdlem109  46235  fourierdlem110  46236  fourierdlem112  46238  fourierdlem113  46239  isomenndlem  46550  hoidmvlelem3  46617  1fzopredsuc  47341  dfclnbgr4  47816  clnbupgr  47825  usgrexmpl2edg  47993  lmod1zr  48415  dftpos5  48780  dftpos6  48781  tposresg  48784  tposrescnv  48785  tposres3  48787