Theorem pssss 4060

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

Syntax hints:   → wi 4   ≠ wne 2964   ⊆ wss 3913   ⊊ wpss 3914

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 210  df-an 401  df-pss 3933

This theorem is referenced by:  pssssd  4062  sspss  4064  pssn2lp  4067  psstr  4070  brrpssg  7720  pssnn  9149  php  9187  php2  9188  php3  9189  findcard3  9239  marypha1lem  9389  infpssr  10288  fin4en1  10289  ssfin4  10290  fin23lem34  10326  npex  10967  elnp  10968  suplem1pr  11033  lsmcv  21239  islbs3  21253  obslbs  21845  spansncvi  31941  chrelati  32653  atcvatlem  32674  satfun  35798  fundmpss  36154  dfon2lem6  36173  finminlem  36714  fvineqsneq  37941  pssexg  42882  xppss12  42885  psshepw  44401