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

Theorem pssss 3271
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 3168 . 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 2446    C_ wss 3152    C. wpss 3153
This theorem is referenced by:  pssssd  3273  sspss  3275  pssn2lp  3277  psstr  3280  brrpssg  6279  php  7045  php2  7046  php3  7047  pssnn  7081  findcard3  7100  marypha1lem  7186  infpssr  7934  fin4en1  7935  ssfin4  7936  fin23lem34  7972  npex  8610  elnp  8611  suplem1pr  8676  wuncn  8792  lsmcv  15894  islbs3  15908  obslbs  16630  spansncvi  22231  chrelati  22944  atcvatlem  22965  fundmpss  24122  dfon2lem6  24144  finminlem  26231
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 3168
  Copyright terms: Public domain W3C validator