Theorem uneq2i 4087

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

Syntax hints:   = wceq 1538   ∪ cun 3879

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886

This theorem is referenced by:  un4  4096  unundir  4098  difdif2  4211  difun2  4387  difdifdir  4395  dfif5  4441  qdass  4649  qdassr  4650  ssunpr  4725  iununi  4984  unidif0  5225  difxp1  5989  unisuc  6235  iunsuc  6241  fresaun  6523  fresaunres2  6524  fvssunirn  6674  fmptap  6909  fvsnun1  6921  funiunfv  6985  onuninsuci  7535  wfrlem13  7950  wfrlem14  7951  wfrlem16  7953  tfrlem10  8006  oarec  8171  dfdom2  8518  fodomr  8652  ranksuc  9278  kmlem3  9563  djuassen  9589  fin1a2lem10  9820  fin1a2lem12  9822  axdc3lem4  9864  prunioo  12859  fz0sn0fz1  13019  facnn  13631  fac0  13632  hashun3  13741  trclublem  14346  dmtrclfv  14369  fsum2dlem  15117  fsumiun  15168  incexclem  15183  fprod2dlem  15326  prmreclem4  16245  phlstr  16645  mreexexlem4d  16910  smndex1basss  18062  smndex1mgm  18064  opsrtoslem2  20724  restcld  21777  neitr  21785  fiuncmp  22009  refun0  22120  1stckgenlem  22158  filconn  22488  ufildr  22536  alexsubALTlem3  22654  ptcmplem1  22657  restmetu  23177  ovolfiniun  24105  unmbl  24141  volfiniun  24151  voliunlem1  24154  plyun0  24794  lgsquadlem3  25966  axlowdimlem3  26738  axlowdimlem17  26752  ex-un  28209  ex-pw  28214  indifundif  30297  iuninc  30324  difico  30532  esum2dlem  31461  fiunelcarsg  31684  carsgclctunlem1  31685  carsggect  31686  bnj601  32302  bnj1416  32421  subfacp1lem1  32539  cvmliftlem10  32654  satf0  32732  frrlem14  33249  noextend  33286  noextendseq  33287  nosupbday  33318  nosupbnd1  33327  nosupbnd2  33329  noetalem2  33331  noetalem3  33332  noetalem4  33333  poimirlem4  35061  poimirlem18  35075  poimirlem21  35078  poimirlem22  35079  poimirlem25  35082  mbfresfi  35103  asindmre  35140  fsuppssind  39459  mapfzcons  39657  mapfzcons1  39658  diophin  39713  iocunico  40161  rp-fakeuninass  40224  rclexi  40315  rtrclex  40317  dfrtrcl5  40329  dfrcl2  40375  corcltrcl  40440  cotrclrcl  40443  frege109d  40458  frege131d  40465  fiiuncl  41699  cnrefiisp  42472  fourierdlem65  42813  fourierdlem89  42837  fourierdlem90  42838  fourierdlem91  42839  fourierdlem96  42844  fourierdlem97  42845  fourierdlem98  42846  fourierdlem99  42847  fourierdlem100  42848  fourierdlem105  42853  fourierdlem108  42856  fourierdlem109  42857  fourierdlem110  42858  fourierdlem112  42860  fourierdlem113  42861  isomenndlem  43169  hoidmvlelem3  43236  1fzopredsuc  43881  lmod1zr  44902