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

Theorem uneq1i 3636
Description: Inference adding union to the right in a class equality. (Contributed by NM, 30-Aug-1993.)
Hypothesis
Ref Expression
uneq1i.1  |-  A  =  B
Assertion
Ref Expression
uneq1i  |-  ( A  u.  C )  =  ( B  u.  C
)

Proof of Theorem uneq1i
StepHypRef Expression
1 uneq1i.1 . 2  |-  A  =  B
2 uneq1 3633 . 2  |-  ( A  =  B  ->  ( A  u.  C )  =  ( B  u.  C ) )
31, 2ax-mp 5 1  |-  ( A  u.  C )  =  ( B  u.  C
)
Colors of variables: wff setvar class
Syntax hints:    = wceq 1381    u. cun 3456
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-v 3095  df-un 3463
This theorem is referenced by:  un12  3644  unundi  3647  undif1  3885  dfif5  3938  tpcoma  4107  qdass  4110  qdassr  4111  tpidm12  4112  unidif0  4606  difxp2  5419  resasplit  5741  fresaun  5742  fresaunres2  5743  df2o3  7141  sbthlem6  7630  fodomr  7666  domss2  7674  domunfican  7791  kmlem11  8538  hashfun  12469  prmreclem2  14307  setscom  14534  gsummptfzsplitl  16822  uniioombllem3  21860  lhop  22283  usgrafilem1  24276  constr3pthlem1  24520  ex-un  25010  ex-pw  25015  subfacp1lem1  28489  dftrpred4g  29285  symdifV  29443  lineunray  29765  fourierdlem80  31854  usgfislem1  32278  usgfisALTlem1  32282  lmod1  32803  bnj1415  33801  bj-2upln1upl  34294
  Copyright terms: Public domain W3C validator