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

Theorem pssss 3598
Description: A proper subclass is a subclass. Theorem 10 of [Suppes] p. 23. (Contributed by NM, 7-Feb-1996.)
Assertion
Ref Expression
pssss

Proof of Theorem pssss
StepHypRef Expression
1 df-pss 3491 . 2
21simplbi 460 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =/=wne 2652  C_wss 3475  C.wpss 3476
This theorem is referenced by:  pssssd  3600  sspss  3602  pssn2lp  3604  psstr  3607  brrpssg  6582  php  7721  php2  7722  php3  7723  pssnn  7758  findcard3  7783  marypha1lem  7913  infpssr  8709  fin4en1  8710  ssfin4  8711  fin23lem34  8747  npex  9385  elnp  9386  suplem1pr  9451  lsmcv  17787  islbs3  17801  obslbs  18761  spansncvi  26570  chrelati  27283  atcvatlem  27304  fundmpss  29196  dfon2lem6  29220  finminlem  30136  psshepw  37811
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