Theorem uneq1i 3796

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

Syntax hints:   = wceq 1523   ∪ cun 3605

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-un 3612

This theorem is referenced by:  un12  3804  unundi  3807  undif1  4076  dfif5  4135  tpcoma  4317  qdass  4320  qdassr  4321  tpidm12  4322  symdifv  4630  unidif0  4868  difxp2  5595  resasplit  6112  fresaun  6113  fresaunres2  6114  df2o3  7618  sbthlem6  8116  fodomr  8152  domss2  8160  domunfican  8274  kmlem11  9020  hashfun  13262  prmreclem2  15668  setscom  15950  gsummptfzsplitl  18379  uniioombllem3  23399  lhop  23824  ex-un  27411  ex-pw  27416  indifundif  29482  bnj1415  31232  subfacp1lem1  31287  dftrpred4g  31858  lineunray  32379  bj-2upln1upl  33137  poimirlem3  33542  poimirlem4  33543  poimirlem5  33544  poimirlem16  33555  poimirlem17  33556  poimirlem19  33558  poimirlem20  33559  poimirlem22  33561  dfrcl2  38283  iunrelexp0  38311  trclfvdecomr  38337  corcltrcl  38348  cotrclrcl  38351  df3o2  38639  fourierdlem80  40721  caragenuncllem  41047  carageniuncllem1  41056  1fzopredsuc  41659  nnsum4primeseven  42013  nnsum4primesevenALTV  42014  lmod1  42606