Theorem pssss 4053

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

This proof depends on syntax axioms:   → wi 4   ≠ wne 2960   ⊆ wss 3906   ⊊ wpss 3907

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-pss 3926

This theorem is used by:  pssssd  4055  sspss  4057  pssn2lp  4060  psstr  4063  brrpssg  7732  pssnn  9160  php  9198  php2  9199  php3  9200  findcard3  9250  marypha1lem  9400  infpssr  10307  fin4en1  10308  ssfin4  10309  fin23lem34  10345  npex  10986  elnp  10987  suplem1pr  11052  lsmcv  21315  islbs3  21329  obslbs  21930  spansncvi  32075  chrelati  32787  atcvatlem  32808  satfun  35940  fundmpss  36296  dfon2lem6  36315  finminlem  36886  fvineqsneq  38115  pssexg  43055  xppss12  43058  psshepw  44572