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

Theorem unssad 4158
Description: If (𝐴𝐵) is contained in 𝐶, so is 𝐴. One-way deduction form of unss 4155. Partial converse of unssd 4157. (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 4155 . . 3 ((𝐴𝐶𝐵𝐶) ↔ (𝐴𝐵) ⊆ 𝐶)
31, 2sylibr 234 . 2 (𝜑 → (𝐴𝐶𝐵𝐶))
43simpld 494 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  cun 3914  wss 3916
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-un 3921  df-ss 3933
This theorem is referenced by:  naddcllem  8642  ersym  8685  findcard2d  9135  finsschain  9316  r0weon  9971  ackbij1lem16  10193  wunex2  10697  sumsplit  15740  fsumabs  15773  fsumiun  15793  mrieqvlemd  17596  yonedalem1  18239  yonedalem21  18240  yonedalem22  18245  yonffthlem  18249  lsmsp  20999  mplcoe1  21950  mdetunilem9  22513  ordtbas  23085  isufil2  23801  ufileu  23812  filufint  23813  fmfnfm  23851  flimclslem  23877  fclsfnflim  23920  flimfnfcls  23921  imasdsf1olem  24267  limcdif  25783  jensenlem1  26903  jensenlem2  26904  jensen  26905  gsumvsca1  33185  gsumvsca2  33186  qsdrngilem  33471  fldgenfldext  33669  evls1fldgencl  33671  fldextrspunlem1  33676  fldextrspunfld  33677  algextdeglem1  33713  algextdeglem2  33714  algextdeglem3  33715  algextdeglem4  33716  constrextdg2lem  33744  constrllcllem  33748  constrlccllem  33749  constrcccllem  33750  ordtconnlem1  33920  ssmcls  35554  mclsppslem  35570  rngunsnply  43151  mptrcllem  43595  clcnvlem  43605  brtrclfv2  43709  isotone1  44030  dvnprodlem1  45937
  Copyright terms: Public domain W3C validator