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

Theorem unssad 3676
Description: If  ( A  u.  B ) is contained in  C, so is  A. One-way deduction form of unss 3673. Partial converse of unssd 3675. (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 3673 . . 3  |-  ( ( A  C_  C  /\  B  C_  C )  <->  ( A  u.  B )  C_  C
)
31, 2sylibr 212 . 2  |-  ( ph  ->  ( A  C_  C  /\  B  C_  C ) )
43simpld 459 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    u. cun 3469    C_ wss 3471
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1963  ax-ext 2440
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2612  df-v 3110  df-un 3476  df-in 3478  df-ss 3485
This theorem is referenced by:  ersym  7315  findcard2d  7753  finsschain  7818  r0weon  8381  ackbij1lem16  8606  wunex2  9107  sumsplit  13534  fsumabs  13566  fsumiun  13586  mrieqvlemd  14875  yonedalem1  15390  yonedalem21  15391  yonedalem22  15396  yonffthlem  15400  lsmsp  17510  mplcoe1  17893  mdetunilem9  18884  ordtbas  19454  isufil2  20139  ufileu  20150  filufint  20151  fmfnfm  20189  flimclslem  20215  fclsfnflim  20258  flimfnfcls  20259  imasdsf1olem  20606  mbfeqalem  21779  limcdif  22010  jensenlem1  23039  jensenlem2  23040  jensen  23041  gsumvsca1  27424  gsumvsca2  27425  ordtconlem1  27530  rngunsnply  30718
  Copyright terms: Public domain W3C validator