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

Theorem pssss 3444
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 3338 . 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 4    =/= wne 2601    C_ wss 3322    C. wpss 3323
This theorem is referenced by:  pssssd  3446  sspss  3448  pssn2lp  3450  psstr  3453  brrpssg  6526  php  7293  php2  7294  php3  7295  pssnn  7329  findcard3  7352  marypha1lem  7440  infpssr  8190  fin4en1  8191  ssfin4  8192  fin23lem34  8228  npex  8865  elnp  8866  suplem1pr  8931  lsmcv  16215  islbs3  16229  obslbs  16959  spansncvi  23156  chrelati  23869  atcvatlem  23890  fundmpss  25392  dfon2lem6  25417  finminlem  26323
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 179  df-an 362  df-pss 3338
  Copyright terms: Public domain W3C validator