Theorem uneq1i 4127

Description: Inference adding union to the right in a class equality. (Contributed by NM, 30-Aug-1993.)

Hypothesis

Ref	Expression
uneq1i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
uneq1i	⊢ (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶)

Proof of Theorem uneq1i

Step	Hyp	Ref	Expression
1		uneq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		uneq1 4124	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶)

Syntax hints:   = wceq 1540   ∪ cun 3912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-un 3919

This theorem is referenced by:  un12  4136  unundi  4139  undif1  4439  dfif5  4505  tpcoma  4714  qdass  4717  qdassr  4718  tpidm12  4719  symdifv  5050  unidif0  5315  cnvimassrndm  6125  difxp2  6139  resasplit  6730  fresaun  6731  fresaunres2  6732  f1ofvswap  7281  df2o3  8442  sbthlem6  9056  fodomr  9092  domss2  9100  domunfican  9272  fodomfir  9279  kmlem11  10114  hashfun  14402  prmreclem2  16888  setscom  17150  gsummptfzsplitl  19863  dfcnfldOLD  21280  uniioombllem3  25486  lhop  25921  sltlpss  27819  slelss  27820  addsasslem1  27910  mulsproplem5  28023  mulsproplem6  28024  mulsproplem7  28025  mulsproplem8  28026  ex-un  30353  ex-pw  30358  3unrab  32432  indifundif  32453  nn0split01  32742  cycpmrn  33100  bnj1415  35028  subfacp1lem1  35166  lineunray  36135  bj-2upln1upl  37012  poimirlem3  37617  poimirlem4  37618  poimirlem5  37619  poimirlem16  37630  poimirlem17  37631  poimirlem19  37633  poimirlem20  37634  poimirlem22  37636  df3o2  43302  omcl3g  43323  dfrcl2  43663  iunrelexp0  43691  trclfvdecomr  43717  corcltrcl  43728  cotrclrcl  43731  fourierdlem80  46184  caragenuncllem  46510  carageniuncllem1  46519  1fzopredsuc  47325  nnsum4primeseven  47801  nnsum4primesevenALTV  47802  cycl3grtri  47946  usgrexmpl1edg  48015  usgrexmpl2edg  48020  gpgprismgr4cycllem7  48091  lmod1  48481  tposresg  48866  iscnrm3rlem1  48928