Theorem pssss 4052

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

Syntax hints:   → wi 4   ≠ wne 2958   ⊆ wss 3905   ⊊ wpss 3906

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 3925

This theorem is referenced by:  pssssd  4054  sspss  4056  pssn2lp  4059  psstr  4062  brrpssg  7722  pssnn  9149  php  9187  php2  9188  php3  9189  findcard3  9239  marypha1lem  9389  infpssr  10287  fin4en1  10288  ssfin4  10289  fin23lem34  10325  npex  10966  elnp  10967  suplem1pr  11032  lsmcv  21265  islbs3  21279  obslbs  21880  spansncvi  32004  chrelati  32716  atcvatlem  32737  satfun  35903  fundmpss  36259  dfon2lem6  36278  finminlem  36829  fvineqsneq  38058  pssexg  42997  xppss12  43000  psshepw  44514