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

Theorem unssad 4012
Description: If (𝐴𝐵) is contained in 𝐶, so is 𝐴. One-way deduction form of unss 4009. Partial converse of unssd 4011. (Contributed by David Moews, 1-May-2017.)
Hypothesis
Ref Expression
unssad.1 (𝜑 → (𝐴𝐵) ⊆ 𝐶)
Assertion
Ref Expression
unssad (𝜑𝐴𝐶)

Proof of Theorem unssad
StepHypRef Expression
1 unssad.1 . . 3 (𝜑 → (𝐴𝐵) ⊆ 𝐶)
2 unss 4009 . . 3 ((𝐴𝐶𝐵𝐶) ↔ (𝐴𝐵) ⊆ 𝐶)
31, 2sylibr 226 . 2 (𝜑 → (𝐴𝐶𝐵𝐶))
43simpld 490 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 386  cun 3789  wss 3791
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-9 2115  ax-10 2134  ax-11 2149  ax-12 2162  ax-ext 2753
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2763  df-cleq 2769  df-clel 2773  df-nfc 2920  df-v 3399  df-un 3796  df-in 3798  df-ss 3805
This theorem is referenced by:  ersym  8038  findcard2d  8490  finsschain  8561  r0weon  9168  ackbij1lem16  9392  wunex2  9895  sumsplit  14904  fsumabs  14937  fsumiun  14957  mrieqvlemd  16675  yonedalem1  17298  yonedalem21  17299  yonedalem22  17304  yonffthlem  17308  lsmsp  19481  mplcoe1  19862  mdetunilem9  20831  ordtbas  21404  isufil2  22120  ufileu  22131  filufint  22132  fmfnfm  22170  flimclslem  22196  fclsfnflim  22239  flimfnfcls  22240  imasdsf1olem  22586  limcdif  24077  jensenlem1  25165  jensenlem2  25166  jensen  25167  gsumvsca1  30344  gsumvsca2  30345  ordtconnlem1  30568  ssmcls  32063  mclsppslem  32079  rngunsnply  38684  mptrcllem  38859  clcnvlem  38869  brtrclfv2  38958  isotone1  39284  dvnprodlem1  41071
  Copyright terms: Public domain W3C validator