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

Theorem unssad 3468
Description: If  ( A  u.  B ) is contained in  C, so is  A. One-way deduction form of unss 3465. Partial converse of unssd 3467. (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 3465 . . 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 3262    C_ wss 3264
This theorem is referenced by:  ersym  6854  finsschain  7349  r0weon  7828  ackbij1lem16  8049  wunex2  8547  sumsplit  12480  fsumabs  12508  fsumiun  12528  mrieqvlemd  13782  yonedalem1  14297  yonedalem21  14298  yonedalem22  14303  yonffthlem  14307  lsmsp  16086  mplcoe1  16456  ordtbas  17179  isufil2  17862  ufileu  17873  filufint  17874  fmfnfm  17912  flimclslem  17938  fclsfnflim  17981  flimfnfcls  17982  imasdsf1olem  18312  mbfeqalem  19402  limcdif  19631  jensenlem1  20693  jensenlem2  20694  jensen  20695  rngunsnply  27048
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2375  df-cleq 2381  df-clel 2384  df-nfc 2513  df-v 2902  df-un 3269  df-in 3271  df-ss 3278
  Copyright terms: Public domain W3C validator