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 ⊢ (𝐶 ∪ 𝐴) = (𝐶 ∪ 𝐵)

Syntax hints:   = wceq 1570   ∪ cun 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3910

This theorem is referenced by:  un4  4128  unundir  4130  difdif2  4249  difun2  4442  difdifdir  4452  dfif5  4504  qdass  4719  qdassr  4720  ssunpr  4799  iununi  5065  unidif0  5330  unidif0OLD  5331  difxp1  6162  iunsuc  6448  fresaun  6749  fresaunres2  6750  fmptap  7168  fvsnun1  7180  funiunfv  7246  onuninsuci  7832  frrlem14  8292  tfrlem10  8370  oarec  8543  dfdom2  8971  fodomr  9112  fodomfir  9283  ranksuc  9833  kmlem3  10132  djuassen  10158  fin1a2lem10  10388  fin1a2lem12  10390  axdc3lem4  10432  prunioo  13503  fz0sn0fz1  13669  facnn  14307  fac0  14308  hashun3  14416  trclublem  15028  dmtrclfv  15051  fsum2dlem  15817  fsumiun  15869  incexclem  15886  fprod2dlem  16030  prmreclem4  16974  phlstr  17394  mreexexlem4d  17698  smndex1basss  18962  smndex1mgm  18964  opsrtoslem2  22207  restcld  23329  neitr  23337  fiuncmp  23561  refun0  23672  1stckgenlem  23710  filconn  24040  ufildr  24088  alexsubALTlem3  24206  ptcmplem1  24209  restmetu  24727  ovolfiniun  25660  unmbl  25696  volfiniun  25706  voliunlem1  25709  plyun0  26354  lgsquadlem3  27546  noextend  27830  noextendseq  27831  nosupbday  27869  nosupbnd1  27878  nosupbnd2  27880  noinfbday  27884  noinfbnd1  27893  noinfbnd2  27895  noetasuplem2  27898  noetasuplem3  27899  noetasuplem4  27900  noetainflem4  27904  madeun  28077  addsproplem2  28163  addsasslem1  28196  addsasslem2  28197  negsproplem2  28222  negsproplem6  28226  negsid  28234  mulsproplem2  28310  mulsproplem3  28311  mulsproplem4  28312  mulsproplem12  28320  mulsproplem13  28321  mulsproplem14  28322  mulsass  28359  precsexlemcbv  28399  onmulscl  28471  axlowdimlem3  29294  axlowdimlem17  29308  ex-un  30775  ex-pw  30780  indifundif  32870  iuninc  32905  difico  33128  esum2dlem  34482  fiunelcarsg  34706  carsgclctunlem1  34707  carsggect  34708  bnj601  35308  bnj1416  35427  subfacp1lem1  35671  cvmliftlem10  35786  satf0  35864  poimirlem4  38275  poimirlem18  38289  poimirlem21  38292  poimirlem22  38293  poimirlem25  38296  mbfresfi  38317  asindmre  38354  dmuncnvepres  39040  blockadjliftmap  39107  fsuppssind  43325  mapfzcons  43447  mapfzcons1  43448  diophin  43503  iocunico  43938  rp-fakeuninass  44242  rclexi  44341  rtrclex  44343  dfrtrcl5  44355  dfrcl2  44400  corcltrcl  44465  cotrclrcl  44468  frege109d  44483  frege131d  44490  nregmodelf1o  45724  fiiuncl  45785  cnrefiisp  46544  fourierdlem65  46885  fourierdlem89  46909  fourierdlem90  46910  fourierdlem91  46911  fourierdlem96  46916  fourierdlem97  46917  fourierdlem98  46918  fourierdlem99  46919  fourierdlem100  46920  fourierdlem105  46925  fourierdlem108  46928  fourierdlem109  46929  fourierdlem110  46930  fourierdlem112  46932  fourierdlem113  46933  isomenndlem  47244  hoidmvlelem3  47311  1fzopredsuc  48062  dfclnbgr4  48589  clnbupgr  48598  usgrexmpl2edg  48794  lmod1zr  49273  dftpos5  49652  dftpos6  49653  tposresg  49656  tposrescnv  49657  tposres3  49659