Theorem uneq2i 3726

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

Syntax hints:   = wceq 1475   ∪ cun 3538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-un 3545

This theorem is referenced by:  un4  3735  unundir  3737  difdif2  3843  difun2  4000  difdifdir  4008  dfif5  4052  qdass  4232  qdassr  4233  ssunpr  4305  iununi  4546  unidif0  4764  difxp1  5478  unisuc  5718  iunsuc  5724  fresaun  5988  fresaunres2  5989  fvssunirn  6127  fmptap  6341  fvsnun1  6353  funiunfv  6410  onuninsuci  6932  wfrlem13  7314  wfrlem14  7315  wfrlem16  7317  tfrlem10  7370  oarec  7529  dfdom2  7867  fodomr  7996  ranksuc  8611  kmlem3  8857  fin1a2lem10  9114  fin1a2lem12  9116  axdc3lem4  9158  prunioo  12172  fz0sn0fz1  12325  facnn  12924  fac0  12925  hashun3  13034  trclublem  13582  dmtrclfv  13607  fsum2dlem  14343  fsumiun  14394  incexclem  14407  fprod2dlem  14549  prmreclem4  15461  strlemor1  15796  strlemor2  15797  strlemor3  15798  phlstr  15857  mreexexlem4d  16130  opsrtoslem2  19306  restcld  20786  neitr  20794  fiuncmp  21017  refun0  21128  1stckgenlem  21166  filcon  21497  ufildr  21545  alexsubALTlem3  21663  ptcmplem1  21666  restmetu  22185  ovolfiniun  23076  unmbl  23112  volfiniun  23122  voliunlem1  23125  plyun0  23757  lgsquadlem3  24907  axlowdimlem3  25624  axlowdimlem17  25638  usgrafilem1  25940  constr3trllem3  26180  constr3pthlem1  26183  ex-un  26673  ex-pw  26678  indifundif  28740  iuninc  28761  difico  28935  esum2dlem  29481  fiunelcarsg  29705  carsgclctunlem1  29706  carsggect  29707  bnj601  30244  bnj1416  30361  subfacp1lem1  30415  cvmliftlem10  30530  poimirlem4  32583  poimirlem18  32597  poimirlem21  32600  poimirlem22  32601  poimirlem25  32604  mbfresfi  32626  asindmre  32665  mapfzcons  36297  mapfzcons1  36298  diophin  36354  iocunico  36815  rp-fakeuninass  36881  rclexi  36941  rtrclex  36943  dfrtrcl5  36955  dfrcl2  36985  corcltrcl  37050  cotrclrcl  37053  frege109d  37068  frege131d  37075  fiiuncl  38259  fourierdlem65  39064  fourierdlem89  39088  fourierdlem90  39089  fourierdlem91  39090  fourierdlem96  39095  fourierdlem97  39096  fourierdlem98  39097  fourierdlem99  39098  fourierdlem100  39099  fourierdlem105  39104  fourierdlem108  39107  fourierdlem109  39108  fourierdlem110  39109  fourierdlem112  39111  fourierdlem113  39112  isomenndlem  39420  hoidmvlelem3  39487  1fzopredsuc  39947  lmod1zr  42076