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

Theorem unssad 4160
Description: If (𝐴𝐵) is contained in 𝐶, so is 𝐴. One-way deduction form of unss 4157. Partial converse of unssd 4159. (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 4157 . . 3 ((𝐴𝐶𝐵𝐶) ↔ (𝐴𝐵) ⊆ 𝐶)
31, 2sylibr 235 . 2 (𝜑 → (𝐴𝐶𝐵𝐶))
43simpld 495 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  cun 3931  wss 3933
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-v 3494  df-un 3938  df-in 3940  df-ss 3949
This theorem is referenced by:  ersym  8290  findcard2d  8748  finsschain  8819  r0weon  9426  ackbij1lem16  9645  wunex2  10148  sumsplit  15111  fsumabs  15144  fsumiun  15164  mrieqvlemd  16888  yonedalem1  17510  yonedalem21  17511  yonedalem22  17516  yonffthlem  17520  lsmsp  19787  mplcoe1  20174  mdetunilem9  21157  ordtbas  21728  isufil2  22444  ufileu  22455  filufint  22456  fmfnfm  22494  flimclslem  22520  fclsfnflim  22563  flimfnfcls  22564  imasdsf1olem  22910  limcdif  24401  jensenlem1  25491  jensenlem2  25492  jensen  25493  gsumvsca1  30781  gsumvsca2  30782  ordtconnlem1  31066  ssmcls  32711  mclsppslem  32727  rngunsnply  39651  mptrcllem  39851  clcnvlem  39861  brtrclfv2  39950  isotone1  40276  dvnprodlem1  42107
  Copyright terms: Public domain W3C validator