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

Theorem uneq1i 3325
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 3322 . 2  |-  ( A  =  B  ->  ( A  u.  C )  =  ( B  u.  C ) )
31, 2ax-mp 8 1  |-  ( A  u.  C )  =  ( B  u.  C
)
Colors of variables: wff set class
Syntax hints:    = wceq 1623    u. cun 3150
This theorem is referenced by:  un12  3333  unundi  3336  undif1  3529  dfif5  3577  tpcoma  3723  qdass  3726  qdassr  3727  tpidm12  3728  unidif0  4183  resasplit  5411  fresaun  5412  fresaunres2  5413  difxp2  6155  df2o3  6492  sbthlem6  6976  fodomr  7012  domss2  7020  domunfican  7129  kmlem11  7786  hashfun  11389  prmreclem2  12964  setscom  13176  uniioombllem3  18940  lhop  19363  ex-un  20811  ex-pw  20816  fmptpr  23214  subfacp1lem1  23710  dftrpred4g  24237  symdifV  24369  lineunray  24770  bnj1415  29068
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-un 3157
  Copyright terms: Public domain W3C validator