Theorem pssss 4047

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

Syntax hints:   → wi 4   ≠ wne 2929   ⊆ wss 3898   ⊊ wpss 3899

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 3918

This theorem is referenced by:  pssssd  4049  sspss  4051  pssn2lp  4053  psstr  4056  brrpssg  7667  pssnn  9089  php  9127  php2  9128  php3  9129  findcard3  9178  marypha1lem  9328  infpssr  10210  fin4en1  10211  ssfin4  10212  fin23lem34  10248  npex  10888  elnp  10889  suplem1pr  10954  lsmcv  21087  islbs3  21101  obslbs  21676  spansncvi  31653  chrelati  32365  atcvatlem  32386  satfun  35527  fundmpss  35883  dfon2lem6  35902  finminlem  36434  fvineqsneq  37529  pssexg  42397  xppss12  42400  psshepw  43945