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

Theorem pssssd 3600
Description: Deduce subclass from proper subclass. (Contributed by NM, 29-Feb-1996.)
Hypothesis
Ref Expression
pssssd.1
Assertion
Ref Expression
pssssd

Proof of Theorem pssssd
StepHypRef Expression
1 pssssd.1 . 2
2 pssss 3598 . 2
31, 2syl 16 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  C_wss 3475  C.wpss 3476
This theorem is referenced by:  fin23lem36  8749  fin23lem39  8751  canthnumlem  9047  canthp1lem2  9052  elprnq  9390  npomex  9395  prlem934  9432  ltexprlem7  9441  wuncn  9568  mrieqv2d  15036  slwpss  16632  pgpfac1lem5  17130  lbspss  17728  lsppratlem1  17793  lsppratlem3  17795  lsppratlem4  17796  lrelat  34739  lsatcvatlem  34774
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 371  df-pss 3491
  Copyright terms: Public domain W3C validator