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

Theorem unssad 3934
Description: If (𝐴𝐵) is contained in 𝐶, so is 𝐴. One-way deduction form of unss 3931. Partial converse of unssd 3933. (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 3931 . . 3 ((𝐴𝐶𝐵𝐶) ↔ (𝐴𝐵) ⊆ 𝐶)
31, 2sylibr 224 . 2 (𝜑 → (𝐴𝐶𝐵𝐶))
43simpld 477 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  cun 3714  wss 3716
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2048  df-clab 2748  df-cleq 2754  df-clel 2757  df-nfc 2892  df-v 3343  df-un 3721  df-in 3723  df-ss 3730
This theorem is referenced by:  ersym  7926  findcard2d  8370  finsschain  8441  r0weon  9046  ackbij1lem16  9270  wunex2  9773  sumsplit  14719  fsumabs  14753  fsumiun  14773  mrieqvlemd  16512  yonedalem1  17134  yonedalem21  17135  yonedalem22  17140  yonffthlem  17144  lsmsp  19309  mplcoe1  19688  mdetunilem9  20649  ordtbas  21219  isufil2  21934  ufileu  21945  filufint  21946  fmfnfm  21984  flimclslem  22010  fclsfnflim  22053  flimfnfcls  22054  imasdsf1olem  22400  mbfeqalem  23629  limcdif  23860  jensenlem1  24934  jensenlem2  24935  jensen  24936  gsumvsca1  30113  gsumvsca2  30114  ordtconnlem1  30301  ssmcls  31793  mclsppslem  31809  rngunsnply  38264  mptrcllem  38441  clcnvlem  38451  brtrclfv2  38540  isotone1  38867  dvnprodlem1  40683
  Copyright terms: Public domain W3C validator