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

Theorem unssbd 3789
Description: If (𝐴𝐵) is contained in 𝐶, so is 𝐵. One-way deduction form of unss 3785. Partial converse of unssd 3787. (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 3785 . . 3 ((𝐴𝐶𝐵𝐶) ↔ (𝐴𝐵) ⊆ 𝐶)
31, 2sylibr 224 . 2 (𝜑 → (𝐴𝐶𝐵𝐶))
43simprd 479 1 (𝜑𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  cun 3570  wss 3572
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-v 3200  df-un 3577  df-in 3579  df-ss 3586
This theorem is referenced by:  eldifpw  6973  ertr  7754  finsschain  8270  r0weon  8832  ackbij1lem16  9054  wunfi  9540  wunex2  9557  hashf1lem2  13235  sumsplit  14493  fsum2dlem  14495  fsumabs  14527  fsumrlim  14537  fsumo1  14538  fsumiun  14547  fprod2dlem  14704  mreexexlem3d  16300  yonedalem1  16906  yonedalem21  16907  yonedalem3a  16908  yonedalem4c  16911  yonedalem22  16912  yonedalem3b  16913  yonedainv  16915  yonffthlem  16916  ablfac1eulem  18465  lsmsp  19080  lsppratlem3  19143  mplcoe1  19459  mdetunilem9  20420  filufint  21718  fmfnfmlem4  21755  hausflim  21779  fclsfnflim  21825  fsumcn  22667  mbfeqalem  23403  itgfsum  23587  jensenlem1  24707  jensenlem2  24708  gsumvsca1  29767  gsumvsca2  29768  ordtconnlem1  29955  vhmcls  31448  mclsppslem  31465  rngunsnply  37569  brtrclfv2  37845
  Copyright terms: Public domain W3C validator