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

Theorem pssss 3273
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 3170 . 2  |-  ( A 
C.  B  <->  ( A  C_  B  /\  A  =/= 
B ) )
21simplbi 448 1  |-  ( A 
C.  B  ->  A  C_  B )
Colors of variables: wff set class
Syntax hints:    -> wi 6    =/= wne 2448    C_ wss 3154    C. wpss 3155
This theorem is referenced by:  pssssd  3275  sspss  3277  pssn2lp  3279  psstr  3282  brrpssg  6241  php  7041  php2  7042  php3  7043  pssnn  7077  findcard3  7096  marypha1lem  7182  infpssr  7930  fin4en1  7931  ssfin4  7932  fin23lem34  7968  npex  8606  elnp  8607  suplem1pr  8672  wuncn  8788  lsmcv  15889  islbs3  15903  obslbs  16625  spansncvi  22224  chrelati  22937  atcvatlem  22958  fundmpss  23524  dfon2lem6  23546  finminlem  25631
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
This theorem depends on definitions:  df-bi 179  df-an 362  df-pss 3170
  Copyright terms: Public domain W3C validator