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

Theorem pssssd 3436
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 3434 . 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 3312    C. wpss 3313
This theorem is referenced by:  fin23lem36  8220  fin23lem39  8222  canthnumlem  8515  canthp1lem2  8520  elprnq  8860  npomex  8865  prlem934  8902  ltexprlem7  8911  wuncn  9037  mrieqv2d  13856  slwpss  15238  pgpfac1lem5  15629  lbspss  16146  lsppratlem1  16211  lsppratlem3  16213  lsppratlem4  16214  lrelat  29749  lsatcvatlem  29784
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 3328
  Copyright terms: Public domain W3C validator