Theorem pssss 4043

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

Syntax hints:   → wi 4   ≠ wne 2928   ⊆ wss 3897   ⊊ wpss 3898

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 3917

This theorem is referenced by:  pssssd  4045  sspss  4047  pssn2lp  4049  psstr  4052  brrpssg  7653  pssnn  9073  php  9111  php2  9112  php3  9113  findcard3  9162  marypha1lem  9312  infpssr  10194  fin4en1  10195  ssfin4  10196  fin23lem34  10232  npex  10872  elnp  10873  suplem1pr  10938  lsmcv  21073  islbs3  21087  obslbs  21662  spansncvi  31624  chrelati  32336  atcvatlem  32357  satfun  35447  fundmpss  35803  dfon2lem6  35822  finminlem  36352  fvineqsneq  37446  pssexg  42259  xppss12  42262  psshepw  43821