Theorem pssss 4039

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

Syntax hints:   → wi 4   ≠ wne 2933   ⊆ wss 3890   ⊊ wpss 3891

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 3910

This theorem is referenced by:  pssssd  4041  sspss  4043  pssn2lp  4045  psstr  4048  brrpssg  7672  pssnn  9096  php  9134  php2  9135  php3  9136  findcard3  9186  marypha1lem  9339  infpssr  10221  fin4en1  10222  ssfin4  10223  fin23lem34  10259  npex  10900  elnp  10901  suplem1pr  10966  lsmcv  21131  islbs3  21145  obslbs  21720  spansncvi  31738  chrelati  32450  atcvatlem  32471  satfun  35609  fundmpss  35965  dfon2lem6  35984  finminlem  36516  fvineqsneq  37742  pssexg  42681  xppss12  42684  psshepw  44233