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

Theorem unssad 4188
Description: If (𝐴𝐵) is contained in 𝐶, so is 𝐴. One-way deduction form of unss 4185. Partial converse of unssd 4187. (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 4185 . . 3 ((𝐴𝐶𝐵𝐶) ↔ (𝐴𝐵) ⊆ 𝐶)
31, 2sylibr 233 . 2 (𝜑 → (𝐴𝐶𝐵𝐶))
43simpld 493 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394  cun 3945  wss 3947
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-v 3464  df-un 3952  df-ss 3964
This theorem is referenced by:  naddcllem  8706  ersym  8746  findcard2d  9204  finsschain  9403  r0weon  10055  ackbij1lem16  10278  wunex2  10781  sumsplit  15772  fsumabs  15805  fsumiun  15825  mrieqvlemd  17642  yonedalem1  18297  yonedalem21  18298  yonedalem22  18303  yonffthlem  18307  lsmsp  21064  mplcoe1  22044  mdetunilem9  22613  ordtbas  23187  isufil2  23903  ufileu  23914  filufint  23915  fmfnfm  23953  flimclslem  23979  fclsfnflim  24022  flimfnfcls  24023  imasdsf1olem  24370  limcdif  25896  jensenlem1  27015  jensenlem2  27016  jensen  27017  gsumvsca1  33090  gsumvsca2  33091  qsdrngilem  33369  fldgenfldext  33554  evls1fldgencl  33556  algextdeglem1  33584  algextdeglem2  33585  algextdeglem3  33586  algextdeglem4  33587  ordtconnlem1  33739  ssmcls  35395  mclsppslem  35411  rngunsnply  42834  mptrcllem  43280  clcnvlem  43290  brtrclfv2  43394  isotone1  43715  dvnprodlem1  45567
  Copyright terms: Public domain W3C validator