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

Theorem unssbd 3926
Description: If (𝐴𝐵) is contained in 𝐶, so is 𝐵. One-way deduction form of unss 3922. Partial converse of unssd 3924. (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 3922 . . 3 ((𝐴𝐶𝐵𝐶) ↔ (𝐴𝐵) ⊆ 𝐶)
31, 2sylibr 224 . 2 (𝜑 → (𝐴𝐶𝐵𝐶))
43simprd 482 1 (𝜑𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  cun 3705  wss 3707
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-v 3334  df-un 3712  df-in 3714  df-ss 3721
This theorem is referenced by:  eldifpw  7133  ertr  7918  finsschain  8430  r0weon  9017  ackbij1lem16  9241  wunfi  9727  wunex2  9744  hashf1lem2  13424  sumsplit  14690  fsum2dlem  14692  fsumabs  14724  fsumrlim  14734  fsumo1  14735  fsumiun  14744  fprod2dlem  14901  mreexexlem3d  16500  yonedalem1  17105  yonedalem21  17106  yonedalem3a  17107  yonedalem4c  17110  yonedalem22  17111  yonedalem3b  17112  yonedainv  17114  yonffthlem  17115  ablfac1eulem  18663  lsmsp  19280  lsppratlem3  19343  mplcoe1  19659  mdetunilem9  20620  filufint  21917  fmfnfmlem4  21954  hausflim  21978  fclsfnflim  22024  fsumcn  22866  mbfeqalem  23600  itgfsum  23784  jensenlem1  24904  jensenlem2  24905  gsumvsca1  30083  gsumvsca2  30084  ordtconnlem1  30271  vhmcls  31762  mclsppslem  31779  rngunsnply  38237  brtrclfv2  38513
  Copyright terms: Public domain W3C validator