Theorem pssss 4064

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

Syntax hints:   → wi 4   ≠ wne 2926   ⊆ wss 3917   ⊊ wpss 3918

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 207  df-an 396  df-pss 3937

This theorem is referenced by:  pssssd  4066  sspss  4068  pssn2lp  4070  psstr  4073  brrpssg  7704  pssnn  9138  php  9177  php2  9178  php3  9179  findcard3  9236  findcard3OLD  9237  marypha1lem  9391  infpssr  10268  fin4en1  10269  ssfin4  10270  fin23lem34  10306  npex  10946  elnp  10947  suplem1pr  11012  lsmcv  21058  islbs3  21072  obslbs  21646  spansncvi  31588  chrelati  32300  atcvatlem  32321  satfun  35405  fundmpss  35761  dfon2lem6  35783  finminlem  36313  fvineqsneq  37407  pssexg  42221  xppss12  42224  psshepw  43784