Theorem pssss 4096

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

Syntax hints:   → wi 4   ≠ wne 2941   ⊆ wss 3949   ⊊ wpss 3950

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 206  df-an 398  df-pss 3968

This theorem is referenced by:  pssssd  4098  sspss  4100  pssn2lp  4102  psstr  4105  brrpssg  7715  pssnn  9168  php  9210  php2  9211  php3  9212  phpOLD  9222  php2OLD  9223  php3OLD  9224  pssnnOLD  9265  findcard3  9285  findcard3OLD  9286  marypha1lem  9428  infpssr  10303  fin4en1  10304  ssfin4  10305  fin23lem34  10341  npex  10981  elnp  10982  suplem1pr  11047  lsmcv  20754  islbs3  20768  obslbs  21285  spansncvi  30905  chrelati  31617  atcvatlem  31638  satfun  34402  fundmpss  34738  dfon2lem6  34760  finminlem  35203  fvineqsneq  36293  pssexg  41044  xppss12  41047  psshepw  42539