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

Theorem pssss 4015
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 3890 . 2 (𝐴𝐵 ↔ (𝐴𝐵𝐴𝐵))
21simplbi 501 1 (𝐴𝐵𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wne 2940  wss 3871  wpss 3872
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 210  df-an 400  df-pss 3890
This theorem is referenced by:  pssssd  4017  sspss  4019  pssn2lp  4021  psstr  4024  brrpssg  7518  php  8835  php2  8836  php3  8837  pssnn  8851  pssnnOLD  8900  findcard3  8919  marypha1lem  9054  infpssr  9927  fin4en1  9928  ssfin4  9929  fin23lem34  9965  npex  10605  elnp  10606  suplem1pr  10671  lsmcv  20183  islbs3  20197  obslbs  20697  spansncvi  29738  chrelati  30450  atcvatlem  30471  satfun  33091  fundmpss  33464  dfon2lem6  33488  finminlem  34249  fvineqsneq  35325  pssexg  39922  xppss12  39925  psshepw  41081
  Copyright terms: Public domain W3C validator