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

Theorem pssss 3551
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 3444 . 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 2644    C_ wss 3428    C. wpss 3429
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 3444
This theorem is referenced by:  pssssd  3553  sspss  3555  pssn2lp  3557  psstr  3560  brrpssg  6464  php  7597  php2  7598  php3  7599  pssnn  7634  findcard3  7658  marypha1lem  7786  infpssr  8580  fin4en1  8581  ssfin4  8582  fin23lem34  8618  npex  9258  elnp  9259  suplem1pr  9324  lsmcv  17330  islbs3  17344  obslbs  18266  spansncvi  25192  chrelati  25905  atcvatlem  25926  fundmpss  27713  dfon2lem6  27737  finminlem  28653
  Copyright terms: Public domain W3C validator