Theorem uneq1i 4089

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

Syntax hints:   = wceq 1539   ∪ cun 3881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-un 3888

This theorem is referenced by:  un12  4097  unundi  4100  undif1  4406  dfif5  4472  tpcoma  4683  qdass  4686  qdassr  4687  tpidm12  4688  symdifv  5011  unidif0  5277  cnvimassrndm  6044  difxp2  6058  resasplit  6628  fresaun  6629  fresaunres2  6630  f1ofvswap  7158  df2o3  8282  sbthlem6  8828  fodomr  8864  domss2  8872  domunfican  9017  dftrpred4g  9413  kmlem11  9847  hashfun  14080  prmreclem2  16546  setscom  16809  gsummptfzsplitl  19449  uniioombllem3  24654  lhop  25085  ex-un  28689  ex-pw  28694  indifundif  30774  cycpmrn  31312  bnj1415  32918  subfacp1lem1  33041  sltlpss  34014  lineunray  34376  bj-2upln1upl  35141  poimirlem3  35707  poimirlem4  35708  poimirlem5  35709  poimirlem16  35720  poimirlem17  35721  poimirlem19  35723  poimirlem20  35724  poimirlem22  35726  metakunt24  40076  dfrcl2  41171  iunrelexp0  41199  trclfvdecomr  41225  corcltrcl  41236  cotrclrcl  41239  df3o2  41523  fourierdlem80  43617  caragenuncllem  43940  carageniuncllem1  43949  1fzopredsuc  44704  nnsum4primeseven  45140  nnsum4primesevenALTV  45141  lmod1  45721  iscnrm3rlem1  46122