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

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

Proof of Theorem pssss
StepHypRef Expression
1 df-pss 3143 . 2  |-  ( A 
C.  B  <->  ( A  C_  B  /\  A  =/= 
B ) )
21simplbi 448 1  |-  ( A 
C.  B  ->  A  C_  B )
Colors of variables: wff set class
Syntax hints:    -> wi 6    =/= wne 2421    C_ wss 3127    C. wpss 3128
This theorem is referenced by:  pssssd  3248  sspss  3250  pssn2lp  3252  psstr  3255  brrpssg  6213  php  7013  php2  7014  php3  7015  pssnn  7049  findcard3  7068  marypha1lem  7154  infpssr  7902  fin4en1  7903  ssfin4  7904  fin23lem34  7940  npex  8578  elnp  8579  suplem1pr  8644  wuncn  8760  lsmcv  15856  islbs3  15870  obslbs  16592  spansncvi  22191  chrelati  22904  atcvatlem  22925  fundmpss  23491  dfon2lem6  23513  finminlem  25598
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
This theorem depends on definitions:  df-bi 179  df-an 362  df-pss 3143
  Copyright terms: Public domain W3C validator