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 2733

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 2740  df-cleq 2753  df-clel 2836  df-v 3453  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  5322  difxp2  6157  cnvimassrndmOLD  6198  resasplit  6750  fresaun  6751  fresaunres2  6752  xpsntpg  7142  f1ofvswap  7312  df2o3  8477  sbthlem6  9104  fodomr  9140  domss2  9148  domunfican  9306  fodomfir  9312  kmlem11  10232  hashfun  14575  prmreclem2  17088  setscom  17351  gsummptfzsplitl  20140  uniioombllem3  25899  lhop  26329  ltslpss  28287  leslss  28288  addsasslem1  28382  mulsproplem5  28499  mulsproplem6  28500  mulsproplem7  28501  mulsproplem8  28502  ex-un  31018  ex-pw  31023  3unrab  33092  indifundif  33113  partfun2  33263  nn0split01  33402  cycpmrn  33697  evlextv  34167  esplyind  34200  esplyindfv  34201  vietalem  34204  bnj1415  35661  subfacp1lem1  35923  lineunray  36892  ttcun  37280  ttciun  37282  bj-2upln1upl  37917  poimirlem3  38521  poimirlem4  38522  poimirlem5  38523  poimirlem16  38534  poimirlem17  38535  poimirlem19  38537  poimirlem20  38538  poimirlem22  38540  dmxrnuncnvepres  39304  df3o2  44299  omcl3g  44320  dfrcl2  44659  iunrelexp0  44687  trclfvdecomr  44713  corcltrcl  44724  cotrclrcl  44727  fourierdlem80  47165  caragenuncllem  47491  carageniuncllem1  47500  1fzopredsuc  48364  nnsum4primeseven  48867  nnsum4primesevenALTV  48868  cycl3grtri  49014  usgrexmpl1edg  49091  usgrexmpl2edg  49096  gpgprismgr4cycllem7  49168  lmod1  49573  tposresg  49955  iscnrm3rlem1  50017