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

Theorem pssssd 3273
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 3271 . 2  |-  ( A 
C.  B  ->  A  C_  B )
31, 2syl 15 1  |-  ( ph  ->  A  C_  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    C_ wss 3152    C. wpss 3153
This theorem is referenced by:  fin23lem36  7974  fin23lem39  7976  canthnumlem  8270  canthp1lem2  8275  elprnq  8615  npomex  8620  prlem934  8657  ltexprlem7  8666  mrieqv2d  13541  slwpss  14923  pgpfac1lem5  15314  lbspss  15835  lsppratlem1  15900  lsppratlem3  15902  lsppratlem4  15903  lrelat  29204  lsatcvatlem  29239
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 177  df-an 360  df-pss 3168
  Copyright terms: Public domain W3C validator