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

Theorem pssss 3378
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 3272 . 2  |-  ( A 
C.  B  <->  ( A  C_  B  /\  A  =/= 
B ) )
21simplbi 447 1  |-  ( A 
C.  B  ->  A  C_  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    =/= wne 2543    C_ wss 3256    C. wpss 3257
This theorem is referenced by:  pssssd  3380  sspss  3382  pssn2lp  3384  psstr  3387  brrpssg  6453  php  7220  php2  7221  php3  7222  pssnn  7256  findcard3  7279  marypha1lem  7366  infpssr  8114  fin4en1  8115  ssfin4  8116  fin23lem34  8152  npex  8789  elnp  8790  suplem1pr  8855  lsmcv  16133  islbs3  16147  obslbs  16873  spansncvi  22995  chrelati  23708  atcvatlem  23729  fundmpss  25139  dfon2lem6  25161  finminlem  26005
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 178  df-an 361  df-pss 3272
  Copyright terms: Public domain W3C validator