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

Theorem pssss 4091
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 3964 . 2 (𝐴𝐵 ↔ (𝐴𝐵𝐴𝐵))
21simplbi 496 1 (𝐴𝐵𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wne 2929  wss 3944  wpss 3945
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 206  df-an 395  df-pss 3964
This theorem is referenced by:  pssssd  4093  sspss  4095  pssn2lp  4097  psstr  4100  brrpssg  7731  pssnn  9196  php  9238  php2  9239  php3  9240  phpOLD  9250  php2OLD  9251  php3OLD  9252  pssnnOLD  9293  findcard3  9313  findcard3OLD  9314  marypha1lem  9463  infpssr  10338  fin4en1  10339  ssfin4  10340  fin23lem34  10376  npex  11016  elnp  11017  suplem1pr  11082  lsmcv  21046  islbs3  21060  obslbs  21686  spansncvi  31539  chrelati  32251  atcvatlem  32272  satfun  35154  fundmpss  35495  dfon2lem6  35517  finminlem  35935  fvineqsneq  37024  pssexg  41850  xppss12  41853  psshepw  43362
  Copyright terms: Public domain W3C validator