Theorem uneq1i 4104

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

Syntax hints:   = wceq 1542   ∪ cun 3887

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-un 3894

This theorem is referenced by:  un12  4113  unundi  4116  undif1  4416  dfif5  4483  tpcoma  4694  qdass  4697  qdassr  4698  tpidm12  4699  symdifv  5028  unidif0OLD  5302  cnvimassrndm  6116  difxp2  6130  resasplit  6710  fresaun  6711  fresaunres2  6712  f1ofvswap  7261  df2o3  8413  sbthlem6  9030  fodomr  9066  domss2  9074  domunfican  9232  fodomfir  9238  kmlem11  10083  hashfun  14399  prmreclem2  16888  setscom  17150  gsummptfzsplitl  19908  uniioombllem3  25552  lhop  25983  ltslpss  27900  leslss  27901  addsasslem1  27995  mulsproplem5  28112  mulsproplem6  28113  mulsproplem7  28114  mulsproplem8  28115  ex-un  30494  ex-pw  30499  3unrab  32573  indifundif  32594  partfun2  32749  nn0split01  32891  cycpmrn  33204  evlextv  33686  esplyind  33719  esplyindfv  33720  vietalem  33723  bnj1415  35180  subfacp1lem1  35361  lineunray  36329  ttcun  36694  ttciun  36696  bj-2upln1upl  37331  poimirlem3  37944  poimirlem4  37945  poimirlem5  37946  poimirlem16  37957  poimirlem17  37958  poimirlem19  37960  poimirlem20  37961  poimirlem22  37963  dmxrnuncnvepres  38713  df3o2  43741  omcl3g  43762  dfrcl2  44101  iunrelexp0  44129  trclfvdecomr  44155  corcltrcl  44166  cotrclrcl  44169  fourierdlem80  46614  caragenuncllem  46940  carageniuncllem1  46949  1fzopredsuc  47773  nnsum4primeseven  48276  nnsum4primesevenALTV  48277  cycl3grtri  48423  usgrexmpl1edg  48500  usgrexmpl2edg  48505  gpgprismgr4cycllem7  48577  lmod1  48968  tposresg  49353  iscnrm3rlem1  49415