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 ⊢ (𝐴 ∪ 𝐶) = (𝐵 ∪ 𝐶)

This proof depends on syntax axioms:   = wceq 1570   ∪ cun 3904

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3911

This theorem is used by:  un12  4126  unundi  4129  undif1  4437  dfif5  4506  tpcoma  4718  qdass  4721  qdassr  4722  tpidm12  4723  symdifv  5054  unidif0OLD  5333  cnvimassrndm  6151  difxp2  6165  resasplit  6752  fresaun  6753  fresaunres2  6754  f1ofvswap  7310  df2o3  8463  sbthlem6  9083  fodomr  9119  domss2  9127  domunfican  9284  fodomfir  9290  kmlem11  10156  hashfun  14488  prmreclem2  16995  setscom  17258  gsummptfzsplitl  20027  uniioombllem3  25775  lhop  26206  ltslpss  28132  leslss  28133  addsasslem1  28227  mulsproplem5  28344  mulsproplem6  28345  mulsproplem7  28346  mulsproplem8  28347  ex-un  30822  ex-pw  30827  3unrab  32896  indifundif  32917  partfun2  33068  nn0split01  33208  cycpmrn  33503  evlextv  33972  esplyind  34005  esplyindfv  34006  vietalem  34009  bnj1415  35467  subfacp1lem1  35684  lineunray  36652  ttcun  37056  ttciun  37058  bj-2upln1upl  37693  poimirlem3  38307  poimirlem4  38308  poimirlem5  38309  poimirlem16  38320  poimirlem17  38321  poimirlem19  38323  poimirlem20  38324  poimirlem22  38326  dmxrnuncnvepres  39074  df3o2  44073  omcl3g  44094  dfrcl2  44433  iunrelexp0  44461  trclfvdecomr  44487  corcltrcl  44498  cotrclrcl  44501  fourierdlem80  46933  caragenuncllem  47259  carageniuncllem1  47268  1fzopredsuc  48095  nnsum4primeseven  48598  nnsum4primesevenALTV  48599  cycl3grtri  48745  usgrexmpl1edg  48822  usgrexmpl2edg  48827  gpgprismgr4cycllem7  48899  lmod1  49305  tposresg  49689  iscnrm3rlem1  49751