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

Theorem pssss 3284
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 3181 . 2  |-  ( A 
C.  B  <->  ( A  C_  B  /\  A  =/= 
B ) )
21simplbi 446 1  |-  ( A 
C.  B  ->  A  C_  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    =/= wne 2459    C_ wss 3165    C. wpss 3166
This theorem is referenced by:  pssssd  3286  sspss  3288  pssn2lp  3290  psstr  3293  brrpssg  6295  php  7061  php2  7062  php3  7063  pssnn  7097  findcard3  7116  marypha1lem  7202  infpssr  7950  fin4en1  7951  ssfin4  7952  fin23lem34  7988  npex  8626  elnp  8627  suplem1pr  8692  wuncn  8808  lsmcv  15910  islbs3  15924  obslbs  16646  spansncvi  22247  chrelati  22960  atcvatlem  22981  fundmpss  24193  dfon2lem6  24215  finminlem  26334
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 177  df-an 360  df-pss 3181
  Copyright terms: Public domain W3C validator