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

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

Proof of Theorem unssad
StepHypRef Expression
1 unssad.1 . . 3  |-  ( ph  ->  ( A  u.  B
)  C_  C )
2 unss 3513 . . 3  |-  ( ( A  C_  C  /\  B  C_  C )  <->  ( A  u.  B )  C_  C
)
31, 2sylibr 204 . 2  |-  ( ph  ->  ( A  C_  C  /\  B  C_  C ) )
43simpld 446 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    u. cun 3310    C_ wss 3312
This theorem is referenced by:  ersym  6909  finsschain  7405  r0weon  7886  ackbij1lem16  8107  wunex2  8605  sumsplit  12544  fsumabs  12572  fsumiun  12592  mrieqvlemd  13846  yonedalem1  14361  yonedalem21  14362  yonedalem22  14367  yonffthlem  14371  lsmsp  16150  mplcoe1  16520  ordtbas  17248  isufil2  17932  ufileu  17943  filufint  17944  fmfnfm  17982  flimclslem  18008  fclsfnflim  18051  flimfnfcls  18052  imasdsf1olem  18395  mbfeqalem  19526  limcdif  19755  jensenlem1  20817  jensenlem2  20818  jensen  20819  rngunsnply  27346
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 2416
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 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-v 2950  df-un 3317  df-in 3319  df-ss 3326
  Copyright terms: Public domain W3C validator