Theorem uneq1i 4073

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

Syntax hints:   = wceq 1543   ∪ cun 3864

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3410  df-un 3871

This theorem is referenced by:  un12  4081  unundi  4084  undif1  4390  dfif5  4455  tpcoma  4666  qdass  4669  qdassr  4670  tpidm12  4671  symdifv  4994  unidif0  5251  cnvimassrndm  6015  difxp2  6029  resasplit  6589  fresaun  6590  fresaunres2  6591  f1ofvswap  7116  df2o3  8217  sbthlem6  8761  fodomr  8797  domss2  8805  domunfican  8944  dftrpred4g  9340  kmlem11  9774  hashfun  14004  prmreclem2  16470  setscom  16733  gsummptfzsplitl  19318  uniioombllem3  24482  lhop  24913  ex-un  28507  ex-pw  28512  indifundif  30592  cycpmrn  31129  bnj1415  32731  subfacp1lem1  32854  sltlpss  33824  lineunray  34186  bj-2upln1upl  34951  poimirlem3  35517  poimirlem4  35518  poimirlem5  35519  poimirlem16  35530  poimirlem17  35531  poimirlem19  35533  poimirlem20  35534  poimirlem22  35536  metakunt24  39870  dfrcl2  40959  iunrelexp0  40987  trclfvdecomr  41013  corcltrcl  41024  cotrclrcl  41027  df3o2  41311  fourierdlem80  43402  caragenuncllem  43725  carageniuncllem1  43734  1fzopredsuc  44489  nnsum4primeseven  44925  nnsum4primesevenALTV  44926  lmod1  45506  iscnrm3rlem1  45907