Theorem uneq1i 4166

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-un 4154

This theorem is used by:  un12  4174  unundi  4177  undif1  4433  dfif5  4502  tpcoma  4713  qdass  4716  qdassr  4717  tpidm12  4718  symdifv  5051  unidif0OLD  5329  difxp2  6175  cnvimassrndmOLD  6218  resasplit  6782  fresaun  6783  fresaunres2  6784  xpsntpg  7176  f1ofvswap  7345  df2o3  8522  sbthlem6  9149  fodomr  9185  domss2  9193  domunfican  9351  fodomfir  9357  kmlem11  10278  hashfun  14623  prmreclem2  17139  setscom  17402  gsummptfzsplitl  20198  uniioombllem3  25961  lhop  26391  ltslpss  28351  leslss  28352  addsasslem1  28446  mulsproplem5  28563  mulsproplem6  28564  mulsproplem7  28565  mulsproplem8  28566  ex-un  31082  ex-pw  31087  3unrab  33198  indifundif  33219  partfun2  33367  nn0split01  33505  cycpmrn  33803  evlextv  34285  esplyind  34318  esplyindfv  34319  vietalem  34322  bnj1415  35779  subfacp1lem1  36152  lineunray  37127  ttcun  37515  ttciun  37517  bj-2upln1upl  38152  poimirlem3  38809  poimirlem4  38810  poimirlem5  38811  poimirlem16  38822  poimirlem17  38823  poimirlem19  38825  poimirlem20  38826  poimirlem22  38828  dmxrnuncnvepres  39590  df3o2  44576  omcl3g  44597  dfrcl2  44935  iunrelexp0  44963  trclfvdecomr  44989  corcltrcl  45000  cotrclrcl  45003  fourierdlem80  47469  caragenuncllem  47795  carageniuncllem1  47804  1fzopredsuc  48668  nnsum4primeseven  49171  nnsum4primesevenALTV  49172  cycl3grtri  49318  usgrexmpl1edg  49395  usgrexmpl2edg  49400  gpgprismgr4cycllem7  49472  lmod1  49935  tposresg  50322  iscnrm3rlem1  50385