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

Theorem unssbd 3621
Description: If  ( A  u.  B ) is contained in  C, so is  B. One-way deduction form of unss 3617. Partial converse of unssd 3619. (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 3617 . . 3  |-  ( ( A  C_  C  /\  B  C_  C )  <->  ( A  u.  B )  C_  C
)
31, 2sylibr 212 . 2  |-  ( ph  ->  ( A  C_  C  /\  B  C_  C ) )
43simprd 461 1  |-  ( ph  ->  B  C_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    u. cun 3412    C_ wss 3414
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-v 3061  df-un 3419  df-in 3421  df-ss 3428
This theorem is referenced by:  eldifpw  6594  ertr  7363  finsschain  7861  r0weon  8422  ackbij1lem16  8647  wunfi  9129  wunex2  9146  hashf1lem2  12554  sumsplit  13734  fsum2dlem  13736  fsumabs  13766  fsumrlim  13776  fsumo1  13777  fsumiun  13786  fprod2dlem  13936  mreexexlem3d  15260  yonedalem1  15865  yonedalem21  15866  yonedalem3a  15867  yonedalem4c  15870  yonedalem22  15871  yonedalem3b  15872  yonedainv  15874  yonffthlem  15875  ablfac1eulem  17443  lsmsp  18052  lsppratlem3  18115  mplcoe1  18447  mdetunilem9  19414  filufint  20713  fmfnfmlem4  20750  hausflim  20774  fclsfnflim  20820  fsumcn  21666  mbfeqalem  22341  itgfsum  22525  jensenlem1  23642  jensenlem2  23643  gsumvsca1  28225  gsumvsca2  28226  ordtconlem1  28359  vhmcls  29778  mclsppslem  29795  rngunsnply  35486  brtrclfv2  35706
  Copyright terms: Public domain W3C validator