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

Theorem pssss 3664
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 3556 . 2 (𝐴𝐵 ↔ (𝐴𝐵𝐴𝐵))
21simplbi 475 1 (𝐴𝐵𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wne 2780  wss 3540  wpss 3541
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 196  df-an 385  df-pss 3556
This theorem is referenced by:  pssssd  3666  sspss  3668  pssn2lp  3670  psstr  3673  brrpssg  6815  php  8007  php2  8008  php3  8009  pssnn  8041  findcard3  8066  marypha1lem  8200  infpssr  8991  fin4en1  8992  ssfin4  8993  fin23lem34  9029  npex  9665  elnp  9666  suplem1pr  9731  lsmcv  18911  islbs3  18925  obslbs  19841  spansncvi  27689  chrelati  28401  atcvatlem  28422  fundmpss  30704  dfon2lem6  30731  finminlem  31276  psshepw  36896
  Copyright terms: Public domain W3C validator