Theorem pssss 4108

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

Syntax hints:   → wi 4   ≠ wne 2938   ⊆ wss 3963   ⊊ wpss 3964

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 3983

This theorem is referenced by:  pssssd  4110  sspss  4112  pssn2lp  4114  psstr  4117  brrpssg  7744  pssnn  9207  php  9245  php2  9246  php3  9247  phpOLD  9257  php2OLD  9258  php3OLD  9259  findcard3  9316  findcard3OLD  9317  marypha1lem  9471  infpssr  10346  fin4en1  10347  ssfin4  10348  fin23lem34  10384  npex  11024  elnp  11025  suplem1pr  11090  lsmcv  21161  islbs3  21175  obslbs  21768  spansncvi  31681  chrelati  32393  atcvatlem  32414  satfun  35396  fundmpss  35748  dfon2lem6  35770  finminlem  36301  fvineqsneq  37395  pssexg  42244  xppss12  42247  psshepw  43778