Theorem pssss 4050

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

Syntax hints:   → wi 4   ≠ wne 2932   ⊆ wss 3901   ⊊ wpss 3902

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 3921

This theorem is referenced by:  pssssd  4052  sspss  4054  pssn2lp  4056  psstr  4059  brrpssg  7670  pssnn  9093  php  9131  php2  9132  php3  9133  findcard3  9183  marypha1lem  9336  infpssr  10218  fin4en1  10219  ssfin4  10220  fin23lem34  10256  npex  10897  elnp  10898  suplem1pr  10963  lsmcv  21096  islbs3  21110  obslbs  21685  spansncvi  31727  chrelati  32439  atcvatlem  32460  satfun  35605  fundmpss  35961  dfon2lem6  35980  finminlem  36512  fvineqsneq  37617  pssexg  42482  xppss12  42485  psshepw  44029