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

Theorem pssss 3406
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 3300 . 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 2571    C_ wss 3284    C. wpss 3285
This theorem is referenced by:  pssssd  3408  sspss  3410  pssn2lp  3412  psstr  3415  brrpssg  6487  php  7254  php2  7255  php3  7256  pssnn  7290  findcard3  7313  marypha1lem  7400  infpssr  8148  fin4en1  8149  ssfin4  8150  fin23lem34  8186  npex  8823  elnp  8824  suplem1pr  8889  lsmcv  16172  islbs3  16186  obslbs  16916  spansncvi  23111  chrelati  23824  atcvatlem  23845  fundmpss  25340  dfon2lem6  25362  finminlem  26215
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 3300
  Copyright terms: Public domain W3C validator