Theorem pssss 4121

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

Syntax hints:   → wi 4   ≠ wne 2946   ⊆ wss 3976   ⊊ wpss 3977

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 3996

This theorem is referenced by:  pssssd  4123  sspss  4125  pssn2lp  4127  psstr  4130  brrpssg  7760  pssnn  9234  php  9273  php2  9274  php3  9275  phpOLD  9285  php2OLD  9286  php3OLD  9287  findcard3  9346  findcard3OLD  9347  marypha1lem  9502  infpssr  10377  fin4en1  10378  ssfin4  10379  fin23lem34  10415  npex  11055  elnp  11056  suplem1pr  11121  lsmcv  21166  islbs3  21180  obslbs  21773  spansncvi  31684  chrelati  32396  atcvatlem  32417  satfun  35379  fundmpss  35730  dfon2lem6  35752  finminlem  36284  fvineqsneq  37378  pssexg  42219  xppss12  42222  psshepw  43750