Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  uneq1i Structured version   Visualization version   GIF version

Theorem uneq1i 4086
 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
StepHypRef Expression
1 uneq1i.1 . 2 𝐴 = 𝐵
2 uneq1 4083 . 2 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
31, 2ax-mp 5 1 (𝐴𝐶) = (𝐵𝐶)
 Colors of variables: wff setvar class Syntax hints:   = wceq 1538   ∪ cun 3879 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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886 This theorem is referenced by:  un12  4094  unundi  4097  undif1  4382  dfif5  4441  tpcoma  4646  qdass  4649  qdassr  4650  tpidm12  4651  symdifv  4971  unidif0  5225  difxp2  5990  resasplit  6522  fresaun  6523  fresaunres2  6524  df2o3  8102  sbthlem6  8618  fodomr  8654  domss2  8662  domunfican  8777  kmlem11  9573  hashfun  13796  prmreclem2  16245  setscom  16521  gsummptfzsplitl  19049  uniioombllem3  24196  lhop  24626  ex-un  28216  ex-pw  28221  indifundif  30304  cycpmrn  30842  bnj1415  32432  subfacp1lem1  32551  dftrpred4g  33198  lineunray  33733  bj-2upln1upl  34476  poimirlem3  35076  poimirlem4  35077  poimirlem5  35078  poimirlem16  35089  poimirlem17  35090  poimirlem19  35092  poimirlem20  35093  poimirlem22  35095  metakunt24  39389  dfrcl2  40390  iunrelexp0  40418  trclfvdecomr  40444  corcltrcl  40455  cotrclrcl  40458  df3o2  40742  fourierdlem80  42843  caragenuncllem  43166  carageniuncllem1  43175  1fzopredsuc  43896  nnsum4primeseven  44333  nnsum4primesevenALTV  44334  lmod1  44915
 Copyright terms: Public domain W3C validator