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

Theorem unssbd 3529
Description: If  ( A  u.  B ) is contained in  C, so is  B. One-way deduction form of unss 3525. Partial converse of unssd 3527. (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 3525 . . 3  |-  ( ( A  C_  C  /\  B  C_  C )  <->  ( A  u.  B )  C_  C
)
31, 2sylibr 212 . 2  |-  ( ph  ->  ( A  C_  C  /\  B  C_  C ) )
43simprd 463 1  |-  ( ph  ->  B  C_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    u. cun 3321    C_ wss 3323
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2969  df-un 3328  df-in 3330  df-ss 3337
This theorem is referenced by:  eldifpw  6383  ertr  7108  finsschain  7610  r0weon  8171  ackbij1lem16  8396  wunfi  8880  wunex2  8897  hashf1lem2  12201  sumsplit  13227  fsum2dlem  13229  fsumabs  13256  fsumrlim  13266  fsumo1  13267  fsumiun  13276  mreexexlem3d  14576  yonedalem1  15074  yonedalem21  15075  yonedalem3a  15076  yonedalem4c  15079  yonedalem22  15080  yonedalem3b  15081  yonedainv  15083  yonffthlem  15084  ablfac1eulem  16561  lsmsp  17144  lsppratlem3  17207  mplcoe1  17521  mdetunilem9  18401  filufint  19468  fmfnfmlem4  19505  hausflim  19529  fclsfnflim  19575  fsumcn  20421  mbfeqalem  21095  itgfsum  21279  jensenlem1  22355  jensenlem2  22356  ordtconlem1  26306  fprod2dlem  27442  rngunsnply  29483
  Copyright terms: Public domain W3C validator