Theorem uneq2i 4161

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

Syntax hints:   = wceq 1542   ∪ cun 3947

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-un 3954

This theorem is referenced by:  un4  4170  unundir  4172  difdif2  4287  difun2  4481  difdifdir  4492  dfif5  4545  qdass  4758  qdassr  4759  ssunpr  4836  iununi  5103  unidif0  5359  difxp1  6165  iunsuc  6450  fresaun  6763  fresaunres2  6764  fvssunirnOLD  6926  fmptap  7168  fvsnun1  7180  funiunfv  7247  onuninsuci  7829  frrlem14  8284  wfrlem13OLD  8321  wfrlem14OLD  8322  wfrlem16OLD  8324  tfrlem10  8387  oarec  8562  dfdom2  8974  fodomr  9128  ranksuc  9860  kmlem3  10147  djuassen  10173  fin1a2lem10  10404  fin1a2lem12  10406  axdc3lem4  10448  prunioo  13458  fz0sn0fz1  13618  facnn  14235  fac0  14236  hashun3  14344  trclublem  14942  dmtrclfv  14965  fsum2dlem  15716  fsumiun  15767  incexclem  15782  fprod2dlem  15924  prmreclem4  16852  phlstr  17291  mreexexlem4d  17591  smndex1basss  18786  smndex1mgm  18788  opsrtoslem2  21617  restcld  22676  neitr  22684  fiuncmp  22908  refun0  23019  1stckgenlem  23057  filconn  23387  ufildr  23435  alexsubALTlem3  23553  ptcmplem1  23556  restmetu  24079  ovolfiniun  25018  unmbl  25054  volfiniun  25064  voliunlem1  25067  plyun0  25711  lgsquadlem3  26885  noextend  27169  noextendseq  27170  nosupbday  27208  nosupbnd1  27217  nosupbnd2  27219  noinfbday  27223  noinfbnd1  27232  noinfbnd2  27234  noetasuplem2  27237  noetasuplem3  27238  noetasuplem4  27239  noetainflem4  27243  madeun  27379  addsproplem2  27456  addsasslem1  27489  addsasslem2  27490  negsproplem2  27506  negsproplem6  27510  negsid  27518  mulsproplem2  27576  mulsproplem3  27577  mulsproplem4  27578  mulsproplem12  27586  mulsproplem13  27587  mulsproplem14  27588  mulsass  27624  precsexlemcbv  27655  axlowdimlem3  28233  axlowdimlem17  28247  ex-un  29708  ex-pw  29713  indifundif  31793  iuninc  31823  difico  32025  esum2dlem  33121  fiunelcarsg  33346  carsgclctunlem1  33347  carsggect  33348  bnj601  33962  bnj1416  34081  subfacp1lem1  34201  cvmliftlem10  34316  satf0  34394  poimirlem4  36540  poimirlem18  36554  poimirlem21  36557  poimirlem22  36558  poimirlem25  36561  mbfresfi  36582  asindmre  36619  fsuppssind  41213  mapfzcons  41502  mapfzcons1  41503  diophin  41558  iocunico  42008  rp-fakeuninass  42315  rclexi  42414  rtrclex  42416  dfrtrcl5  42428  dfrcl2  42473  corcltrcl  42538  cotrclrcl  42541  frege109d  42556  frege131d  42563  fiiuncl  43800  cnrefiisp  44594  fourierdlem65  44935  fourierdlem89  44959  fourierdlem90  44960  fourierdlem91  44961  fourierdlem96  44966  fourierdlem97  44967  fourierdlem98  44968  fourierdlem99  44969  fourierdlem100  44970  fourierdlem105  44975  fourierdlem108  44978  fourierdlem109  44979  fourierdlem110  44980  fourierdlem112  44982  fourierdlem113  44983  isomenndlem  45294  hoidmvlelem3  45361  1fzopredsuc  46080  lmod1zr  47222