Theorem uneq1i 4118

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

Syntax hints:   = wceq 1570   ∪ cun 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3910

This theorem is referenced by:  un12  4126  unundi  4129  undif1  4437  dfif5  4504  tpcoma  4716  qdass  4719  qdassr  4720  tpidm12  4721  symdifv  5052  unidif0OLD  5331  cnvimassrndm  6149  difxp2  6163  resasplit  6748  fresaun  6749  fresaunres2  6750  f1ofvswap  7304  df2o3  8457  sbthlem6  9076  fodomr  9112  domss2  9120  domunfican  9277  fodomfir  9283  kmlem11  10140  hashfun  14470  prmreclem2  16972  setscom  17235  gsummptfzsplitl  19998  uniioombllem3  25744  lhop  26175  ltslpss  28101  leslss  28102  addsasslem1  28196  mulsproplem5  28313  mulsproplem6  28314  mulsproplem7  28315  mulsproplem8  28316  ex-un  30775  ex-pw  30780  3unrab  32849  indifundif  32870  partfun2  33021  nn0split01  33162  cycpmrn  33463  evlextv  33932  esplyind  33965  esplyindfv  33966  vietalem  33969  bnj1415  35426  subfacp1lem1  35671  lineunray  36639  ttcun  37023  ttciun  37025  bj-2upln1upl  37660  poimirlem3  38274  poimirlem4  38275  poimirlem5  38276  poimirlem16  38287  poimirlem17  38288  poimirlem19  38290  poimirlem20  38291  poimirlem22  38293  dmxrnuncnvepres  39041  df3o2  44040  omcl3g  44061  dfrcl2  44400  iunrelexp0  44428  trclfvdecomr  44454  corcltrcl  44465  cotrclrcl  44468  fourierdlem80  46900  caragenuncllem  47226  carageniuncllem1  47235  1fzopredsuc  48062  nnsum4primeseven  48565  nnsum4primesevenALTV  48566  cycl3grtri  48712  usgrexmpl1edg  48789  usgrexmpl2edg  48794  gpgprismgr4cycllem7  48866  lmod1  49272  tposresg  49656  iscnrm3rlem1  49718