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 1542   ∪ cun 3901

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 2709

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 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-un 3908

This theorem is referenced by:  un12  4127  unundi  4130  undif1  4430  dfif5  4498  tpcoma  4709  qdass  4712  qdassr  4713  tpidm12  4714  symdifv  5043  unidif0  5307  cnvimassrndm  6118  difxp2  6132  resasplit  6712  fresaun  6713  fresaunres2  6714  f1ofvswap  7262  df2o3  8415  sbthlem6  9032  fodomr  9068  domss2  9076  domunfican  9234  fodomfir  9240  kmlem11  10083  hashfun  14372  prmreclem2  16857  setscom  17119  gsummptfzsplitl  19874  dfcnfldOLD  21337  uniioombllem3  25554  lhop  25989  ltslpss  27916  leslss  27917  addsasslem1  28011  mulsproplem5  28128  mulsproplem6  28129  mulsproplem7  28130  mulsproplem8  28131  ex-un  30511  ex-pw  30516  3unrab  32590  indifundif  32611  partfun2  32766  nn0split01  32909  cycpmrn  33237  evlextv  33719  esplyind  33752  esplyindfv  33753  vietalem  33756  bnj1415  35214  subfacp1lem1  35395  lineunray  36363  bj-2upln1upl  37272  poimirlem3  37874  poimirlem4  37875  poimirlem5  37876  poimirlem16  37887  poimirlem17  37888  poimirlem19  37890  poimirlem20  37891  poimirlem22  37893  dmxrnuncnvepres  38643  df3o2  43670  omcl3g  43691  dfrcl2  44030  iunrelexp0  44058  trclfvdecomr  44084  corcltrcl  44095  cotrclrcl  44098  fourierdlem80  46544  caragenuncllem  46870  carageniuncllem1  46879  1fzopredsuc  47684  nnsum4primeseven  48160  nnsum4primesevenALTV  48161  cycl3grtri  48307  usgrexmpl1edg  48384  usgrexmpl2edg  48389  gpgprismgr4cycllem7  48461  lmod1  48852  tposresg  49237  iscnrm3rlem1  49299