Theorem pssss 4057

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

Syntax hints:   → wi 4   ≠ wne 2925   ⊆ wss 3911   ⊊ wpss 3912

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 3931

This theorem is referenced by:  pssssd  4059  sspss  4061  pssn2lp  4063  psstr  4066  brrpssg  7681  pssnn  9109  php  9148  php2  9149  php3  9150  findcard3  9205  findcard3OLD  9206  marypha1lem  9360  infpssr  10237  fin4en1  10238  ssfin4  10239  fin23lem34  10275  npex  10915  elnp  10916  suplem1pr  10981  lsmcv  21027  islbs3  21041  obslbs  21615  spansncvi  31554  chrelati  32266  atcvatlem  32287  satfun  35371  fundmpss  35727  dfon2lem6  35749  finminlem  36279  fvineqsneq  37373  pssexg  42187  xppss12  42190  psshepw  43750