Theorem uneq1i 4174

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

Syntax hints:   = wceq 1537   ∪ cun 3961

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-un 3968

This theorem is referenced by:  un12  4183  unundi  4186  undif1  4482  dfif5  4547  tpcoma  4755  qdass  4758  qdassr  4759  tpidm12  4760  symdifv  5091  unidif0  5366  cnvimassrndm  6174  difxp2  6188  resasplit  6779  fresaun  6780  fresaunres2  6781  f1ofvswap  7326  df2o3  8513  sbthlem6  9127  fodomr  9167  domss2  9175  domunfican  9359  fodomfir  9366  kmlem11  10199  hashfun  14473  prmreclem2  16951  setscom  17214  gsummptfzsplitl  19966  dfcnfldOLD  21398  uniioombllem3  25634  lhop  26070  sltlpss  27960  slelss  27961  addsasslem1  28051  mulsproplem5  28161  mulsproplem6  28162  mulsproplem7  28163  mulsproplem8  28164  ex-un  30453  ex-pw  30458  3unrab  32531  indifundif  32552  nn0split01  32824  cycpmrn  33146  bnj1415  35031  subfacp1lem1  35164  lineunray  36129  bj-2upln1upl  37007  poimirlem3  37610  poimirlem4  37611  poimirlem5  37612  poimirlem16  37623  poimirlem17  37624  poimirlem19  37626  poimirlem20  37627  poimirlem22  37629  metakunt24  42210  df3o2  43303  omcl3g  43324  dfrcl2  43664  iunrelexp0  43692  trclfvdecomr  43718  corcltrcl  43729  cotrclrcl  43732  fourierdlem80  46142  caragenuncllem  46468  carageniuncllem1  46477  1fzopredsuc  47274  nnsum4primeseven  47725  nnsum4primesevenALTV  47726  usgrexmpl1edg  47919  usgrexmpl2edg  47924  lmod1  48338  iscnrm3rlem1  48737