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

Theorem pssss 3735
Description: A proper subclass is a subclass. Theorem 10 of [Suppes] p. 23. (Contributed by NM, 7-Feb-1996.)
Assertion
Ref Expression
pssss (𝐴𝐵𝐴𝐵)

Proof of Theorem pssss
StepHypRef Expression
1 df-pss 3623 . 2 (𝐴𝐵 ↔ (𝐴𝐵𝐴𝐵))
21simplbi 475 1 (𝐴𝐵𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wne 2823  wss 3607  wpss 3608
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 197  df-an 385  df-pss 3623
This theorem is referenced by:  pssssd  3737  sspss  3739  pssn2lp  3741  psstr  3744  brrpssg  6981  php  8185  php2  8186  php3  8187  pssnn  8219  findcard3  8244  marypha1lem  8380  infpssr  9168  fin4en1  9169  ssfin4  9170  fin23lem34  9206  npex  9846  elnp  9847  suplem1pr  9912  lsmcv  19189  islbs3  19203  obslbs  20122  spansncvi  28639  chrelati  29351  atcvatlem  29372  fundmpss  31790  dfon2lem6  31817  finminlem  32437  psshepw  38399
  Copyright terms: Public domain W3C validator