Theorem pssss 4038

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

Step	Hyp	Ref	Expression
1		df-pss 3909	. 2 ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵))
2	1	simplbi 496	1 ⊢ (𝐴 ⊊ 𝐵 → 𝐴 ⊆ 𝐵)

Syntax hints:   → wi 4   ≠ wne 2932   ⊆ wss 3889   ⊊ wpss 3890

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 207  df-an 396  df-pss 3909

This theorem is referenced by:  pssssd  4040  sspss  4042  pssn2lp  4044  psstr  4047  brrpssg  7679  pssnn  9103  php  9141  php2  9142  php3  9143  findcard3  9193  marypha1lem  9346  infpssr  10230  fin4en1  10231  ssfin4  10232  fin23lem34  10268  npex  10909  elnp  10910  suplem1pr  10975  lsmcv  21139  islbs3  21153  obslbs  21710  spansncvi  31723  chrelati  32435  atcvatlem  32456  satfun  35593  fundmpss  35949  dfon2lem6  35968  finminlem  36500  fvineqsneq  37728  pssexg  42667  xppss12  42670  psshepw  44215