Theorem pssss 3702

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

Syntax hints:   → wi 4   ≠ wne 2794   ⊆ wss 3574   ⊊ wpss 3575

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 197  df-an 386  df-pss 3590

This theorem is referenced by:  pssssd  3704  sspss  3706  pssn2lp  3708  psstr  3711  brrpssg  6939  php  8144  php2  8145  php3  8146  pssnn  8178  findcard3  8203  marypha1lem  8339  infpssr  9130  fin4en1  9131  ssfin4  9132  fin23lem34  9168  npex  9808  elnp  9809  suplem1pr  9874  lsmcv  19141  islbs3  19155  obslbs  20074  spansncvi  28511  chrelati  29223  atcvatlem  29244  fundmpss  31664  dfon2lem6  31693  finminlem  32312  psshepw  38082