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

Theorem unssad 4149
Description: If (𝐴𝐵) is contained in 𝐶, so is 𝐴. One-way deduction form of unss 4146. Partial converse of unssd 4148. (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 4146 . . 3 ((𝐴𝐶𝐵𝐶) ↔ (𝐴𝐵) ⊆ 𝐶)
31, 2sylibr 237 . 2 (𝜑 → (𝐴𝐶𝐵𝐶))
43simpld 498 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  cun 3917  wss 3919
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 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-v 3482  df-un 3924  df-in 3926  df-ss 3936
This theorem is referenced by:  ersym  8297  findcard2d  8757  finsschain  8828  r0weon  9436  ackbij1lem16  9655  wunex2  10158  sumsplit  15123  fsumabs  15156  fsumiun  15176  mrieqvlemd  16900  yonedalem1  17522  yonedalem21  17523  yonedalem22  17528  yonffthlem  17532  lsmsp  19858  mplcoe1  20712  mdetunilem9  21232  ordtbas  21803  isufil2  22519  ufileu  22530  filufint  22531  fmfnfm  22569  flimclslem  22595  fclsfnflim  22638  flimfnfcls  22639  imasdsf1olem  22986  limcdif  24485  jensenlem1  25578  jensenlem2  25579  jensen  25580  gsumvsca1  30889  gsumvsca2  30890  ordtconnlem1  31227  ssmcls  32874  mclsppslem  32890  rngunsnply  40037  mptrcllem  40233  clcnvlem  40243  brtrclfv2  40348  isotone1  40674  dvnprodlem1  42518
  Copyright terms: Public domain W3C validator