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

Theorem pssss 3513
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 3405 . 2  |-  ( A 
C.  B  <->  ( A  C_  B  /\  A  =/= 
B ) )
21simplbi 458 1  |-  ( A 
C.  B  ->  A  C_  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    =/= wne 2577    C_ wss 3389    C. wpss 3390
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 369  df-pss 3405
This theorem is referenced by:  pssssd  3515  sspss  3517  pssn2lp  3519  psstr  3522  brrpssg  6481  php  7620  php2  7621  php3  7622  pssnn  7654  findcard3  7678  marypha1lem  7808  infpssr  8601  fin4en1  8602  ssfin4  8603  fin23lem34  8639  npex  9275  elnp  9276  suplem1pr  9341  lsmcv  17900  islbs3  17914  obslbs  18852  spansncvi  26687  chrelati  27399  atcvatlem  27420  fundmpss  29362  dfon2lem6  29385  finminlem  30302  psshepw  38283
  Copyright terms: Public domain W3C validator