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

Theorem unssbd 3518
Description: If  ( A  u.  B ) is contained in  C, so is  B. One-way deduction form of unss 3514. Partial converse of unssd 3516. (Contributed by David Moews, 1-May-2017.)
Hypothesis
Ref Expression
unssad.1  |-  ( ph  ->  ( A  u.  B
)  C_  C )
Assertion
Ref Expression
unssbd  |-  ( ph  ->  B  C_  C )

Proof of Theorem unssbd
StepHypRef Expression
1 unssad.1 . . 3  |-  ( ph  ->  ( A  u.  B
)  C_  C )
2 unss 3514 . . 3  |-  ( ( A  C_  C  /\  B  C_  C )  <->  ( A  u.  B )  C_  C
)
31, 2sylibr 204 . 2  |-  ( ph  ->  ( A  C_  C  /\  B  C_  C ) )
43simprd 450 1  |-  ( ph  ->  B  C_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    u. cun 3311    C_ wss 3313
This theorem is referenced by:  eldifpw  4748  ertr  6913  finsschain  7406  r0weon  7887  ackbij1lem16  8108  wunfi  8589  wunex2  8606  hashf1lem2  11698  sumsplit  12545  fsum2dlem  12547  fsumabs  12573  fsumrlim  12583  fsumo1  12584  fsumiun  12593  mreexexlem3d  13864  yonedalem1  14362  yonedalem21  14363  yonedalem3a  14364  yonedalem4c  14367  yonedalem22  14368  yonedalem3b  14369  yonedainv  14371  yonffthlem  14372  ablfac1eulem  15623  lsmsp  16151  lsppratlem3  16214  mplcoe1  16521  filufint  17945  fmfnfmlem4  17982  hausflim  18006  fclsfnflim  18052  fsumcn  18893  mbfeqalem  19527  itgfsum  19711  jensenlem1  20818  jensenlem2  20819  fprod2dlem  25297  rngunsnply  27347
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-v 2951  df-un 3318  df-in 3320  df-ss 3327
  Copyright terms: Public domain W3C validator