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

Theorem pssss 3192
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 3091 . 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 2412    C_ wss 3078    C. wpss 3079
This theorem is referenced by:  pssssd  3194  sspss  3195  pssn2lp  3197  psstr  3200  brrpssg  6131  php  6930  php2  6931  php3  6932  pssnn  6966  findcard3  6985  marypha1lem  7070  infpssr  7818  fin4en1  7819  ssfin4  7820  fin23lem34  7856  npex  8490  elnp  8491  suplem1pr  8556  wuncn  8672  lsmcv  15729  islbs3  15742  obslbs  16462  spansncvi  22079  chrelati  22774  atcvatlem  22795  fundmpss  23290  dfon2lem6  23312  finminlem  25397
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 3091
  Copyright terms: Public domain W3C validator