Theorem pssss 4098

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

Syntax hints:   → wi 4   ≠ wne 2940   ⊆ wss 3951   ⊊ wpss 3952

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 3971

This theorem is referenced by:  pssssd  4100  sspss  4102  pssn2lp  4104  psstr  4107  brrpssg  7745  pssnn  9208  php  9247  php2  9248  php3  9249  phpOLD  9259  php2OLD  9260  php3OLD  9261  findcard3  9318  findcard3OLD  9319  marypha1lem  9473  infpssr  10348  fin4en1  10349  ssfin4  10350  fin23lem34  10386  npex  11026  elnp  11027  suplem1pr  11092  lsmcv  21143  islbs3  21157  obslbs  21750  spansncvi  31671  chrelati  32383  atcvatlem  32404  satfun  35416  fundmpss  35767  dfon2lem6  35789  finminlem  36319  fvineqsneq  37413  pssexg  42265  xppss12  42268  psshepw  43801