Theorem uneq1i 4144

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

Syntax hints:   = wceq 1539   ∪ cun 3929

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-v 3465  df-un 3936

This theorem is referenced by:  un12  4153  unundi  4156  undif1  4456  dfif5  4522  tpcoma  4730  qdass  4733  qdassr  4734  tpidm12  4735  symdifv  5066  unidif0  5340  cnvimassrndm  6152  difxp2  6166  resasplit  6758  fresaun  6759  fresaunres2  6760  f1ofvswap  7308  df2o3  8496  sbthlem6  9110  fodomr  9150  domss2  9158  domunfican  9343  fodomfir  9350  kmlem11  10183  hashfun  14458  prmreclem2  16937  setscom  17199  gsummptfzsplitl  19919  dfcnfldOLD  21342  uniioombllem3  25556  lhop  25991  sltlpss  27881  slelss  27882  addsasslem1  27972  mulsproplem5  28082  mulsproplem6  28083  mulsproplem7  28084  mulsproplem8  28085  ex-un  30371  ex-pw  30376  3unrab  32450  indifundif  32471  nn0split01  32759  cycpmrn  33102  bnj1415  35011  subfacp1lem1  35143  lineunray  36107  bj-2upln1upl  36984  poimirlem3  37589  poimirlem4  37590  poimirlem5  37591  poimirlem16  37602  poimirlem17  37603  poimirlem19  37605  poimirlem20  37606  poimirlem22  37608  metakunt24  42188  df3o2  43288  omcl3g  43309  dfrcl2  43649  iunrelexp0  43677  trclfvdecomr  43703  corcltrcl  43714  cotrclrcl  43717  fourierdlem80  46158  caragenuncllem  46484  carageniuncllem1  46493  1fzopredsuc  47294  nnsum4primeseven  47745  nnsum4primesevenALTV  47746  cycl3grtri  47872  usgrexmpl1edg  47941  usgrexmpl2edg  47946  lmod1  48367  tposresg  48737  iscnrm3rlem1  48797