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

Theorem pssssd 3286
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 3284 . 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 3165    C. wpss 3166
This theorem is referenced by:  fin23lem36  7990  fin23lem39  7992  canthnumlem  8286  canthp1lem2  8291  elprnq  8631  npomex  8636  prlem934  8673  ltexprlem7  8682  mrieqv2d  13557  slwpss  14939  pgpfac1lem5  15330  lbspss  15851  lsppratlem1  15916  lsppratlem3  15918  lsppratlem4  15919  lrelat  29826  lsatcvatlem  29861
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 3181
  Copyright terms: Public domain W3C validator