Theorem uneq1i 4058

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

Syntax hints:   = wceq 1522   ∪ cun 3859

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1778  ax-4 1792  ax-5 1889  ax-6 1948  ax-7 1993  ax-8 2082  ax-9 2090  ax-10 2111  ax-11 2125  ax-12 2140  ax-ext 2768

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1763  df-nf 1767  df-sb 2042  df-clab 2775  df-cleq 2787  df-clel 2862  df-nfc 2934  df-v 3438  df-un 3866

This theorem is referenced by:  un12  4066  unundi  4069  undif1  4340  dfif5  4399  tpcoma  4595  qdass  4598  qdassr  4599  tpidm12  4600  symdifv  4909  unidif0  5154  difxp2  5902  resasplit  6419  fresaun  6420  fresaunres2  6421  df2o3  7971  sbthlem6  8482  fodomr  8518  domss2  8526  domunfican  8640  kmlem11  9435  hashfun  13646  prmreclem2  16082  setscom  16356  gsummptfzsplitl  18773  uniioombllem3  23869  lhop  24296  ex-un  27887  ex-pw  27892  indifundif  29966  cycpmrn  30414  bnj1415  31916  subfacp1lem1  32028  dftrpred4g  32676  lineunray  33211  bj-2upln1upl  33954  poimirlem3  34439  poimirlem4  34440  poimirlem5  34441  poimirlem16  34452  poimirlem17  34453  poimirlem19  34455  poimirlem20  34456  poimirlem22  34458  dfrcl2  39517  iunrelexp0  39545  trclfvdecomr  39571  corcltrcl  39582  cotrclrcl  39585  df3o2  39872  fourierdlem80  42027  caragenuncllem  42350  carageniuncllem1  42359  1fzopredsuc  43054  nnsum4primeseven  43461  nnsum4primesevenALTV  43462  lmod1  44041