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

Theorem pssss 4069
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 3951 . 2 (𝐴𝐵 ↔ (𝐴𝐵𝐴𝐵))
21simplbi 498 1 (𝐴𝐵𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wne 3013  wss 3933  wpss 3934
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 208  df-an 397  df-pss 3951
This theorem is referenced by:  pssssd  4071  sspss  4073  pssn2lp  4075  psstr  4078  brrpssg  7440  php  8689  php2  8690  php3  8691  pssnn  8724  findcard3  8749  marypha1lem  8885  infpssr  9718  fin4en1  9719  ssfin4  9720  fin23lem34  9756  npex  10396  elnp  10397  suplem1pr  10462  lsmcv  19842  islbs3  19856  obslbs  20802  spansncvi  29356  chrelati  30068  atcvatlem  30089  satfun  32555  fundmpss  32906  dfon2lem6  32930  finminlem  33563  fvineqsneq  34575  pssexg  38990  xppss12  38993  psshepw  40012
  Copyright terms: Public domain W3C validator