Theorem uneq1i 4093

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

Syntax hints:   = wceq 1539   ∪ cun 3885

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-un 3892

This theorem is referenced by:  un12  4101  unundi  4104  undif1  4409  dfif5  4475  tpcoma  4686  qdass  4689  qdassr  4690  tpidm12  4691  symdifv  5015  unidif0  5282  cnvimassrndm  6055  difxp2  6069  resasplit  6644  fresaun  6645  fresaunres2  6646  f1ofvswap  7178  df2o3  8305  sbthlem6  8875  fodomr  8915  domss2  8923  domunfican  9087  kmlem11  9916  hashfun  14152  prmreclem2  16618  setscom  16881  gsummptfzsplitl  19534  uniioombllem3  24749  lhop  25180  ex-un  28788  ex-pw  28793  indifundif  30873  cycpmrn  31410  bnj1415  33018  subfacp1lem1  33141  sltlpss  34087  lineunray  34449  bj-2upln1upl  35214  poimirlem3  35780  poimirlem4  35781  poimirlem5  35782  poimirlem16  35793  poimirlem17  35794  poimirlem19  35796  poimirlem20  35797  poimirlem22  35799  metakunt24  40148  dfrcl2  41282  iunrelexp0  41310  trclfvdecomr  41336  corcltrcl  41347  cotrclrcl  41350  df3o2  41634  fourierdlem80  43727  caragenuncllem  44050  carageniuncllem1  44059  1fzopredsuc  44816  nnsum4primeseven  45252  nnsum4primesevenALTV  45253  lmod1  45833  iscnrm3rlem1  46234