Theorem pssss 3863

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

Syntax hints:   → wi 4   ≠ wne 2937   ⊆ wss 3732   ⊊ wpss 3733

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 198  df-an 385  df-pss 3748

This theorem is referenced by:  pssssd  3865  sspss  3867  pssn2lp  3869  psstr  3872  brrpssg  7137  php  8351  php2  8352  php3  8353  pssnn  8385  findcard3  8410  marypha1lem  8546  infpssr  9383  fin4en1  9384  ssfin4  9385  fin23lem34  9421  npex  10061  elnp  10062  suplem1pr  10127  lsmcv  19414  islbs3  19429  obslbs  20350  spansncvi  28967  chrelati  29679  atcvatlem  29700  fundmpss  32109  dfon2lem6  32136  finminlem  32756  pssexg  37926  xppss12  37929  psshepw  38756