Theorem pssss 3852

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 3739	. 2 ⊢ (𝐴 ⊊ 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ 𝐵))
2	1	simplbi 485	1 ⊢ (𝐴 ⊊ 𝐵 → 𝐴 ⊆ 𝐵)

Syntax hints:   → wi 4   ≠ wne 2943   ⊆ wss 3723   ⊊ wpss 3724

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 197  df-an 383  df-pss 3739

This theorem is referenced by:  pssssd  3854  sspss  3856  pssn2lp  3858  psstr  3861  brrpssg  7086  php  8300  php2  8301  php3  8302  pssnn  8334  findcard3  8359  marypha1lem  8495  infpssr  9332  fin4en1  9333  ssfin4  9334  fin23lem34  9370  npex  10010  elnp  10011  suplem1pr  10076  lsmcv  19355  islbs3  19370  obslbs  20291  spansncvi  28851  chrelati  29563  atcvatlem  29584  fundmpss  32002  dfon2lem6  32029  finminlem  32649  pssexg  37774  xppss12  37777  psshepw  38608