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

Theorem pssss 3604
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 3497 . 2  |-  ( A 
C.  B  <->  ( A  C_  B  /\  A  =/= 
B ) )
21simplbi 460 1  |-  ( A 
C.  B  ->  A  C_  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    =/= wne 2662    C_ wss 3481    C. wpss 3482
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 371  df-pss 3497
This theorem is referenced by:  pssssd  3606  sspss  3608  pssn2lp  3610  psstr  3613  brrpssg  6577  php  7713  php2  7714  php3  7715  pssnn  7750  findcard3  7775  marypha1lem  7905  infpssr  8700  fin4en1  8701  ssfin4  8702  fin23lem34  8738  npex  9376  elnp  9377  suplem1pr  9442  lsmcv  17658  islbs3  17672  obslbs  18630  spansncvi  26393  chrelati  27106  atcvatlem  27127  fundmpss  29123  dfon2lem6  29147  finminlem  30063
  Copyright terms: Public domain W3C validator