Theorem uneq1i 4155

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

Syntax hints:   = wceq 1534   ∪ cun 3942

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-v 3471  df-un 3949

This theorem is referenced by:  un12  4163  unundi  4166  undif1  4471  dfif5  4540  tpcoma  4750  qdass  4753  qdassr  4754  tpidm12  4755  symdifv  5083  unidif0  5354  cnvimassrndm  6150  difxp2  6164  resasplit  6761  fresaun  6762  fresaunres2  6763  f1ofvswap  7309  df2o3  8488  sbthlem6  9106  fodomr  9146  domss2  9154  domunfican  9338  kmlem11  10177  hashfun  14422  prmreclem2  16879  setscom  17142  gsummptfzsplitl  19881  dfcnfldOLD  21288  uniioombllem3  25507  lhop  25942  sltlpss  27826  slelss  27827  addsasslem1  27913  mulsproplem5  28013  mulsproplem6  28014  mulsproplem7  28015  mulsproplem8  28016  ex-un  30227  ex-pw  30232  indifundif  32314  cycpmrn  32858  bnj1415  34659  subfacp1lem1  34779  lineunray  35733  bj-2upln1upl  36493  poimirlem3  37085  poimirlem4  37086  poimirlem5  37087  poimirlem16  37098  poimirlem17  37099  poimirlem19  37101  poimirlem20  37102  poimirlem22  37104  metakunt24  41652  df3o2  42714  omcl3g  42735  dfrcl2  43076  iunrelexp0  43104  trclfvdecomr  43130  corcltrcl  43141  cotrclrcl  43144  fourierdlem80  45546  caragenuncllem  45872  carageniuncllem1  45881  1fzopredsuc  46676  nnsum4primeseven  47112  nnsum4primesevenALTV  47113  lmod1  47532  iscnrm3rlem1  47931