Theorem pssss 3664

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

Syntax hints:   → wi 4   ≠ wne 2780   ⊆ wss 3540   ⊊ wpss 3541

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 196  df-an 385  df-pss 3556

This theorem is referenced by:  pssssd  3666  sspss  3668  pssn2lp  3670  psstr  3673  brrpssg  6837  php  8029  php2  8030  php3  8031  pssnn  8063  findcard3  8088  marypha1lem  8222  infpssr  9013  fin4en1  9014  ssfin4  9015  fin23lem34  9051  npex  9687  elnp  9688  suplem1pr  9753  lsmcv  18962  islbs3  18976  obslbs  19893  spansncvi  27895  chrelati  28607  atcvatlem  28628  fundmpss  30910  dfon2lem6  30937  finminlem  31482  psshepw  37102