Theorem pssss 4061

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

Syntax hints:   → wi 4   ≠ wne 2925   ⊆ wss 3914   ⊊ wpss 3915

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 3934

This theorem is referenced by:  pssssd  4063  sspss  4065  pssn2lp  4067  psstr  4070  brrpssg  7701  pssnn  9132  php  9171  php2  9172  php3  9173  findcard3  9229  findcard3OLD  9230  marypha1lem  9384  infpssr  10261  fin4en1  10262  ssfin4  10263  fin23lem34  10299  npex  10939  elnp  10940  suplem1pr  11005  lsmcv  21051  islbs3  21065  obslbs  21639  spansncvi  31581  chrelati  32293  atcvatlem  32314  satfun  35398  fundmpss  35754  dfon2lem6  35776  finminlem  36306  fvineqsneq  37400  pssexg  42214  xppss12  42217  psshepw  43777