Theorem pssss 4052

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

Syntax hints:   → wi 4   ≠ wne 2933   ⊆ wss 3903   ⊊ wpss 3904

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 3923

This theorem is referenced by:  pssssd  4054  sspss  4056  pssn2lp  4058  psstr  4061  brrpssg  7680  pssnn  9105  php  9143  php2  9144  php3  9145  findcard3  9195  marypha1lem  9348  infpssr  10230  fin4en1  10231  ssfin4  10232  fin23lem34  10268  npex  10909  elnp  10910  suplem1pr  10975  lsmcv  21108  islbs3  21122  obslbs  21697  spansncvi  31740  chrelati  32452  atcvatlem  32473  satfun  35627  fundmpss  35983  dfon2lem6  36002  finminlem  36534  fvineqsneq  37667  pssexg  42598  xppss12  42601  psshepw  44144