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

Theorem unssad 3644
Description: If  ( A  u.  B ) is contained in  C, so is  A. One-way deduction form of unss 3641. Partial converse of unssd 3643. (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 3641 . . 3  |-  ( ( A  C_  C  /\  B  C_  C )  <->  ( A  u.  B )  C_  C
)
31, 2sylibr 216 . 2  |-  ( ph  ->  ( A  C_  C  /\  B  C_  C ) )
43simpld 461 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371    u. cun 3435    C_ wss 3437
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-v 3084  df-un 3442  df-in 3444  df-ss 3451
This theorem is referenced by:  ersym  7381  findcard2d  7817  finsschain  7885  r0weon  8446  ackbij1lem16  8667  wunex2  9165  sumsplit  13822  fsumabs  13854  fsumiun  13874  mrieqvlemd  15528  yonedalem1  16150  yonedalem21  16151  yonedalem22  16156  yonffthlem  16160  lsmsp  18302  mplcoe1  18682  mdetunilem9  19637  ordtbas  20200  isufil2  20915  ufileu  20926  filufint  20927  fmfnfm  20965  flimclslem  20991  fclsfnflim  21034  flimfnfcls  21035  imasdsf1olem  21380  mbfeqalem  22590  limcdif  22823  jensenlem1  23904  jensenlem2  23905  jensen  23906  gsumvsca1  28547  gsumvsca2  28548  ordtconlem1  28732  ssmcls  30207  mclsppslem  30223  rngunsnply  36003  brtrclfv2  36223  dvnprodlem1  37685
  Copyright terms: Public domain W3C validator