Theorem uneq1i 4105

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

Syntax hints:   = wceq 1542   ∪ cun 3888

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 3432  df-un 3895

This theorem is referenced by:  un12  4114  unundi  4117  undif1  4417  dfif5  4484  tpcoma  4695  qdass  4698  qdassr  4699  tpidm12  4700  symdifv  5029  unidif0  5297  cnvimassrndm  6110  difxp2  6124  resasplit  6704  fresaun  6705  fresaunres2  6706  f1ofvswap  7254  df2o3  8406  sbthlem6  9023  fodomr  9059  domss2  9067  domunfican  9225  fodomfir  9231  kmlem11  10074  hashfun  14390  prmreclem2  16879  setscom  17141  gsummptfzsplitl  19899  dfcnfldOLD  21360  uniioombllem3  25562  lhop  25993  ltslpss  27914  leslss  27915  addsasslem1  28009  mulsproplem5  28126  mulsproplem6  28127  mulsproplem7  28128  mulsproplem8  28129  ex-un  30509  ex-pw  30514  3unrab  32588  indifundif  32609  partfun2  32764  nn0split01  32906  cycpmrn  33219  evlextv  33701  esplyind  33734  esplyindfv  33735  vietalem  33738  bnj1415  35196  subfacp1lem1  35377  lineunray  36345  ttcun  36710  ttciun  36712  bj-2upln1upl  37347  poimirlem3  37958  poimirlem4  37959  poimirlem5  37960  poimirlem16  37971  poimirlem17  37972  poimirlem19  37974  poimirlem20  37975  poimirlem22  37977  dmxrnuncnvepres  38727  df3o2  43759  omcl3g  43780  dfrcl2  44119  iunrelexp0  44147  trclfvdecomr  44173  corcltrcl  44184  cotrclrcl  44187  fourierdlem80  46632  caragenuncllem  46958  carageniuncllem1  46967  1fzopredsuc  47785  nnsum4primeseven  48288  nnsum4primesevenALTV  48289  cycl3grtri  48435  usgrexmpl1edg  48512  usgrexmpl2edg  48517  gpgprismgr4cycllem7  48589  lmod1  48980  tposresg  49365  iscnrm3rlem1  49427