Theorem pssss 4072

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

Syntax hints:   → wi 4   ≠ wne 3016   ⊆ wss 3936   ⊊ wpss 3937

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 209  df-an 399  df-pss 3954

This theorem is referenced by:  pssssd  4074  sspss  4076  pssn2lp  4078  psstr  4081  brrpssg  7445  php  8695  php2  8696  php3  8697  pssnn  8730  findcard3  8755  marypha1lem  8891  infpssr  9724  fin4en1  9725  ssfin4  9726  fin23lem34  9762  npex  10402  elnp  10403  suplem1pr  10468  lsmcv  19907  islbs3  19921  obslbs  20868  spansncvi  29423  chrelati  30135  atcvatlem  30156  satfun  32653  fundmpss  33004  dfon2lem6  33028  finminlem  33661  fvineqsneq  34687  pssexg  39105  xppss12  39108  psshepw  40127