Theorem uneq1i 4164

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

Syntax hints:   = wceq 1540   ∪ cun 3949

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-un 3956

This theorem is referenced by:  un12  4173  unundi  4176  undif1  4476  dfif5  4542  tpcoma  4750  qdass  4753  qdassr  4754  tpidm12  4755  symdifv  5086  unidif0  5360  cnvimassrndm  6172  difxp2  6186  resasplit  6778  fresaun  6779  fresaunres2  6780  f1ofvswap  7326  df2o3  8514  sbthlem6  9128  fodomr  9168  domss2  9176  domunfican  9361  fodomfir  9368  kmlem11  10201  hashfun  14476  prmreclem2  16955  setscom  17217  gsummptfzsplitl  19951  dfcnfldOLD  21380  uniioombllem3  25620  lhop  26055  sltlpss  27945  slelss  27946  addsasslem1  28036  mulsproplem5  28146  mulsproplem6  28147  mulsproplem7  28148  mulsproplem8  28149  ex-un  30443  ex-pw  30448  3unrab  32522  indifundif  32543  nn0split01  32819  cycpmrn  33163  bnj1415  35052  subfacp1lem1  35184  lineunray  36148  bj-2upln1upl  37025  poimirlem3  37630  poimirlem4  37631  poimirlem5  37632  poimirlem16  37643  poimirlem17  37644  poimirlem19  37646  poimirlem20  37647  poimirlem22  37649  metakunt24  42229  df3o2  43326  omcl3g  43347  dfrcl2  43687  iunrelexp0  43715  trclfvdecomr  43741  corcltrcl  43752  cotrclrcl  43755  fourierdlem80  46201  caragenuncllem  46527  carageniuncllem1  46536  1fzopredsuc  47336  nnsum4primeseven  47787  nnsum4primesevenALTV  47788  cycl3grtri  47914  usgrexmpl1edg  47983  usgrexmpl2edg  47988  lmod1  48409  tposresg  48778  iscnrm3rlem1  48837