Theorem pssss 4029

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

Syntax hints:   → wi 4   ≠ wne 2934   ⊆ wss 3883   ⊊ wpss 3884

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 208  df-an 397  df-pss 3903

This theorem is referenced by:  pssssd  4031  sspss  4033  pssn2lp  4035  psstr  4038  brrpssg  7668  pssnn  9093  php  9131  php2  9132  php3  9133  findcard3  9183  marypha1lem  9336  infpssr  10221  fin4en1  10222  ssfin4  10223  fin23lem34  10259  npex  10900  elnp  10901  suplem1pr  10966  lsmcv  21134  islbs3  21148  obslbs  21705  spansncvi  31741  chrelati  32453  atcvatlem  32474  satfun  35639  fundmpss  35995  dfon2lem6  36014  finminlem  36546  fvineqsneq  37774  pssexg  42713  xppss12  42716  psshepw  44232