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

Theorem unssbd 4046
Description: If (𝐴𝐵) is contained in 𝐶, so is 𝐵. One-way deduction form of unss 4042. Partial converse of unssd 4044. (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 4042 . . 3 ((𝐴𝐶𝐵𝐶) ↔ (𝐴𝐵) ⊆ 𝐶)
31, 2sylibr 226 . 2 (𝜑 → (𝐴𝐶𝐵𝐶))
43simprd 488 1 (𝜑𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 387  cun 3820  wss 3822
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-ext 2743
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-clab 2752  df-cleq 2764  df-clel 2839  df-nfc 2911  df-v 3410  df-un 3827  df-in 3829  df-ss 3836
This theorem is referenced by:  eldifpw  7305  ertr  8102  finsschain  8624  r0weon  9230  ackbij1lem16  9453  wunfi  9939  wunex2  9956  hashf1lem2  13625  sumsplit  14981  fsum2dlem  14983  fsumabs  15014  fsumrlim  15024  fsumo1  15025  fsumiun  15034  fprod2dlem  15192  mreexexlem3d  16787  yonedalem1  17392  yonedalem21  17393  yonedalem3a  17394  yonedalem4c  17397  yonedalem22  17398  yonedalem3b  17399  yonedainv  17401  yonffthlem  17402  ablfac1eulem  18956  lsmsp  19592  lsppratlem3  19655  mplcoe1  19971  mdetunilem9  20948  filufint  22247  fmfnfmlem4  22284  hausflim  22308  fclsfnflim  22354  fsumcn  23196  itgfsum  24145  jensenlem1  25281  jensenlem2  25282  gsumvsca1  30557  gsumvsca2  30558  ordtconnlem1  30843  vhmcls  32370  mclsppslem  32387  rngunsnply  39207  brtrclfv2  39473
  Copyright terms: Public domain W3C validator