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

Theorem pssssd 3380
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 3378 . 2  |-  ( A 
C.  B  ->  A  C_  B )
31, 2syl 16 1  |-  ( ph  ->  A  C_  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    C_ wss 3256    C. wpss 3257
This theorem is referenced by:  fin23lem36  8154  fin23lem39  8156  canthnumlem  8449  canthp1lem2  8454  elprnq  8794  npomex  8799  prlem934  8836  ltexprlem7  8845  wuncn  8971  mrieqv2d  13784  slwpss  15166  pgpfac1lem5  15557  lbspss  16074  lsppratlem1  16139  lsppratlem3  16141  lsppratlem4  16142  lrelat  29180  lsatcvatlem  29215
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361  df-pss 3272
  Copyright terms: Public domain W3C validator