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

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

Proof of Theorem unssbd
StepHypRef Expression
1 unssad.1 . . 3 (𝜑 → (𝐴𝐵) ⊆ 𝐶)
2 unss 4135 . . 3 ((𝐴𝐶𝐵𝐶) ↔ (𝐴𝐵) ⊆ 𝐶)
31, 2sylibr 237 . 2 (𝜑 → (𝐴𝐶𝐵𝐶))
43simprd 499 1 (𝜑𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  cun 3906  wss 3908
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2794
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2801  df-cleq 2815  df-clel 2894  df-v 3471  df-un 3913  df-in 3915  df-ss 3925
This theorem is referenced by:  eldifpw  7475  ertr  8291  finsschain  8819  r0weon  9427  ackbij1lem16  9646  wunfi  10132  wunex2  10149  hashf1lem2  13810  sumsplit  15114  fsum2dlem  15116  fsumabs  15147  fsumrlim  15157  fsumo1  15158  fsumiun  15167  fprod2dlem  15325  mreexexlem3d  16908  yonedalem1  17513  yonedalem21  17514  yonedalem3a  17515  yonedalem4c  17518  yonedalem22  17519  yonedalem3b  17520  yonedainv  17522  yonffthlem  17523  ablfac1eulem  19185  lsmsp  19849  lsppratlem3  19912  mplcoe1  20703  mdetunilem9  21223  filufint  22523  fmfnfmlem4  22560  hausflim  22584  fclsfnflim  22630  fsumcn  23473  itgfsum  24428  jensenlem1  25570  jensenlem2  25571  gsumvsca1  30885  gsumvsca2  30886  ordtconnlem1  31241  vhmcls  32887  mclsppslem  32904  rngunsnply  40051  brtrclfv2  40362
  Copyright terms: Public domain W3C validator