Theorem pssss 4049

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

Syntax hints:   → wi 4   ≠ wne 2956   ⊆ wss 3902   ⊊ wpss 3903

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 209  df-an 400  df-pss 3922

This theorem is referenced by:  pssssd  4051  sspss  4053  pssn2lp  4056  psstr  4059  brrpssg  7703  pssnn  9131  php  9169  php2  9170  php3  9171  findcard3  9221  marypha1lem  9373  infpssr  10259  fin4en1  10260  ssfin4  10261  fin23lem34  10297  npex  10938  elnp  10939  suplem1pr  11004  lsmcv  21199  islbs3  21213  obslbs  21770  spansncvi  31812  chrelati  32524  atcvatlem  32545  satfun  35722  fundmpss  36078  dfon2lem6  36097  finminlem  36639  fvineqsneq  37867  pssexg  42806  xppss12  42809  psshepw  44325