Theorem pssss 3686

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

Syntax hints:   → wi 4   ≠ wne 2790   ⊆ wss 3560   ⊊ wpss 3561

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 3576

This theorem is referenced by:  pssssd  3688  sspss  3690  pssn2lp  3692  psstr  3695  brrpssg  6904  php  8104  php2  8105  php3  8106  pssnn  8138  findcard3  8163  marypha1lem  8299  infpssr  9090  fin4en1  9091  ssfin4  9092  fin23lem34  9128  npex  9768  elnp  9769  suplem1pr  9834  lsmcv  19081  islbs3  19095  obslbs  20014  spansncvi  28399  chrelati  29111  atcvatlem  29132  fundmpss  31421  dfon2lem6  31447  finminlem  32007  psshepw  37603