Theorem uneq1i 4130

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

Syntax hints:   = wceq 1540   ∪ cun 3915

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-un 3922

This theorem is referenced by:  un12  4139  unundi  4142  undif1  4442  dfif5  4508  tpcoma  4717  qdass  4720  qdassr  4721  tpidm12  4722  symdifv  5053  unidif0  5318  cnvimassrndm  6128  difxp2  6142  resasplit  6733  fresaun  6734  fresaunres2  6735  f1ofvswap  7284  df2o3  8445  sbthlem6  9062  fodomr  9098  domss2  9106  domunfican  9279  fodomfir  9286  kmlem11  10121  hashfun  14409  prmreclem2  16895  setscom  17157  gsummptfzsplitl  19870  dfcnfldOLD  21287  uniioombllem3  25493  lhop  25928  sltlpss  27826  slelss  27827  addsasslem1  27917  mulsproplem5  28030  mulsproplem6  28031  mulsproplem7  28032  mulsproplem8  28033  ex-un  30360  ex-pw  30365  3unrab  32439  indifundif  32460  nn0split01  32749  cycpmrn  33107  bnj1415  35035  subfacp1lem1  35173  lineunray  36142  bj-2upln1upl  37019  poimirlem3  37624  poimirlem4  37625  poimirlem5  37626  poimirlem16  37637  poimirlem17  37638  poimirlem19  37640  poimirlem20  37641  poimirlem22  37643  df3o2  43309  omcl3g  43330  dfrcl2  43670  iunrelexp0  43698  trclfvdecomr  43724  corcltrcl  43735  cotrclrcl  43738  fourierdlem80  46191  caragenuncllem  46517  carageniuncllem1  46526  1fzopredsuc  47329  nnsum4primeseven  47805  nnsum4primesevenALTV  47806  cycl3grtri  47950  usgrexmpl1edg  48019  usgrexmpl2edg  48024  gpgprismgr4cycllem7  48095  lmod1  48485  tposresg  48870  iscnrm3rlem1  48932