MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pssssd Structured version   Unicode version

Theorem pssssd 3537
Description: Deduce subclass from proper subclass. (Contributed by NM, 29-Feb-1996.)
Hypothesis
Ref Expression
pssssd.1  |-  ( ph  ->  A  C.  B )
Assertion
Ref Expression
pssssd  |-  ( ph  ->  A  C_  B )

Proof of Theorem pssssd
StepHypRef Expression
1 pssssd.1 . 2  |-  ( ph  ->  A  C.  B )
2 pssss 3535 . 2  |-  ( A 
C.  B  ->  A  C_  B )
31, 2syl 17 1  |-  ( ph  ->  A  C_  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    C_ wss 3411    C. wpss 3412
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 369  df-pss 3427
This theorem is referenced by:  fin23lem36  8678  fin23lem39  8680  canthnumlem  8974  canthp1lem2  8979  elprnq  9317  npomex  9322  prlem934  9359  ltexprlem7  9368  wuncn  9495  mrieqv2d  15143  slwpss  16846  pgpfac1lem5  17340  lbspss  17938  lsppratlem1  18003  lsppratlem3  18005  lsppratlem4  18006  lrelat  31996  lsatcvatlem  32031
  Copyright terms: Public domain W3C validator