Theorem pssss 4023

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

Syntax hints:   → wi 4   ≠ wne 2987   ⊆ wss 3881   ⊊ wpss 3882

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 210  df-an 400  df-pss 3900

This theorem is referenced by:  pssssd  4025  sspss  4027  pssn2lp  4029  psstr  4032  brrpssg  7431  php  8685  php2  8686  php3  8687  pssnn  8720  findcard3  8745  marypha1lem  8881  infpssr  9719  fin4en1  9720  ssfin4  9721  fin23lem34  9757  npex  10397  elnp  10398  suplem1pr  10463  lsmcv  19906  islbs3  19920  obslbs  20419  spansncvi  29435  chrelati  30147  atcvatlem  30168  satfun  32771  fundmpss  33122  dfon2lem6  33146  finminlem  33779  fvineqsneq  34829  pssexg  39406  xppss12  39409  psshepw  40489