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

Theorem unssad 3788
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
unssad (𝜑𝐴𝐶)

Proof of Theorem unssad
StepHypRef Expression
1 unssad.1 . . 3 (𝜑 → (𝐴𝐵) ⊆ 𝐶)
2 unss 3785 . . 3 ((𝐴𝐶𝐵𝐶) ↔ (𝐴𝐵) ⊆ 𝐶)
31, 2sylibr 224 . 2 (𝜑 → (𝐴𝐶𝐵𝐶))
43simpld 475 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:  ersym  7751  findcard2d  8199  finsschain  8270  r0weon  8832  ackbij1lem16  9054  wunex2  9557  sumsplit  14493  fsumabs  14527  fsumiun  14547  mrieqvlemd  16283  yonedalem1  16906  yonedalem21  16907  yonedalem22  16912  yonffthlem  16916  lsmsp  19080  mplcoe1  19459  mdetunilem9  20420  ordtbas  20990  isufil2  21706  ufileu  21717  filufint  21718  fmfnfm  21756  flimclslem  21782  fclsfnflim  21825  flimfnfcls  21826  imasdsf1olem  22172  mbfeqalem  23403  limcdif  23634  jensenlem1  24707  jensenlem2  24708  jensen  24709  gsumvsca1  29767  gsumvsca2  29768  ordtconnlem1  29955  ssmcls  31449  mclsppslem  31465  rngunsnply  37569  mptrcllem  37746  clcnvlem  37756  brtrclfv2  37845  isotone1  38172  dvnprodlem1  39930
  Copyright terms: Public domain W3C validator