Theorem uneq1i 4124

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

Syntax hints:   = wceq 1541   ∪ cun 3911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3448  df-un 3918

This theorem is referenced by:  un12  4132  unundi  4135  undif1  4440  dfif5  4507  tpcoma  4716  qdass  4719  qdassr  4720  tpidm12  4721  symdifv  5051  unidif0  5320  cnvimassrndm  6109  difxp2  6123  resasplit  6717  fresaun  6718  fresaunres2  6719  f1ofvswap  7257  df2o3  8425  sbthlem6  9039  fodomr  9079  domss2  9087  domunfican  9271  kmlem11  10105  hashfun  14347  prmreclem2  16800  setscom  17063  gsummptfzsplitl  19724  uniioombllem3  24986  lhop  25417  sltlpss  27279  addsasslem1  27354  ex-un  29431  ex-pw  29436  indifundif  31516  cycpmrn  32062  bnj1415  33739  subfacp1lem1  33860  lineunray  34808  bj-2upln1upl  35568  poimirlem3  36154  poimirlem4  36155  poimirlem5  36156  poimirlem16  36167  poimirlem17  36168  poimirlem19  36170  poimirlem20  36171  poimirlem22  36173  metakunt24  40673  df3o2  41706  omcl3g  41727  dfrcl2  42068  iunrelexp0  42096  trclfvdecomr  42122  corcltrcl  42133  cotrclrcl  42136  fourierdlem80  44547  caragenuncllem  44873  carageniuncllem1  44882  1fzopredsuc  45676  nnsum4primeseven  46112  nnsum4primesevenALTV  46113  lmod1  46693  iscnrm3rlem1  47093