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  7723  pssnn  9152  php  9190  php2  9191  php3  9192  findcard3  9242  marypha1lem  9392  infpssr  10291  fin4en1  10292  ssfin4  10293  fin23lem34  10329  npex  10970  elnp  10971  suplem1pr  11036  lsmcv  21242  islbs3  21256  obslbs  21848  spansncvi  31944  chrelati  32656  atcvatlem  32677  satfun  35801  fundmpss  36157  dfon2lem6  36176  finminlem  36717  fvineqsneq  37945  pssexg  42886  xppss12  42889  psshepw  44405