Theorem uneq1i 4111

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

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

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 2147  ax-9 2155  ax-ext 2732

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 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 3904

This theorem is used by:  un12  4119  unundi  4122  undif1  4430  dfif5  4499  tpcoma  4711  qdass  4714  qdassr  4715  tpidm12  4716  symdifv  5046  unidif0OLD  5325  cnvimassrndm  6143  difxp2  6158  resasplit  6745  fresaun  6746  fresaunres2  6747  xpsntpg  7137  f1ofvswap  7307  df2o3  8463  sbthlem6  9090  fodomr  9126  domss2  9134  domunfican  9291  fodomfir  9297  kmlem11  10163  hashfun  14502  prmreclem2  17009  setscom  17272  gsummptfzsplitl  20060  uniioombllem3  25813  lhop  26243  ltslpss  28173  leslss  28174  addsasslem1  28268  mulsproplem5  28385  mulsproplem6  28386  mulsproplem7  28387  mulsproplem8  28388  ex-un  30904  ex-pw  30909  3unrab  32978  indifundif  32999  partfun2  33149  nn0split01  33288  cycpmrn  33583  evlextv  34052  esplyind  34085  esplyindfv  34086  vietalem  34089  bnj1415  35547  subfacp1lem1  35758  lineunray  36727  ttcun  37131  ttciun  37133  bj-2upln1upl  37768  poimirlem3  38372  poimirlem4  38373  poimirlem5  38374  poimirlem16  38385  poimirlem17  38386  poimirlem19  38388  poimirlem20  38389  poimirlem22  38391  dmxrnuncnvepres  39140  df3o2  44154  omcl3g  44175  dfrcl2  44514  iunrelexp0  44542  trclfvdecomr  44568  corcltrcl  44579  cotrclrcl  44582  fourierdlem80  47014  caragenuncllem  47340  carageniuncllem1  47349  1fzopredsuc  48213  nnsum4primeseven  48716  nnsum4primesevenALTV  48717  cycl3grtri  48863  usgrexmpl1edg  48940  usgrexmpl2edg  48945  gpgprismgr4cycllem7  49017  lmod1  49422  tposresg  49804  iscnrm3rlem1  49866