Theorem pssss 4026

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

Syntax hints:   → wi 4   ≠ wne 2942   ⊆ wss 3883   ⊊ wpss 3884

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 396  df-pss 3902

This theorem is referenced by:  pssssd  4028  sspss  4030  pssn2lp  4032  psstr  4035  brrpssg  7556  php  8897  php2  8898  php3  8899  pssnn  8913  pssnnOLD  8969  findcard3  8987  marypha1lem  9122  infpssr  9995  fin4en1  9996  ssfin4  9997  fin23lem34  10033  npex  10673  elnp  10674  suplem1pr  10739  lsmcv  20318  islbs3  20332  obslbs  20847  spansncvi  29915  chrelati  30627  atcvatlem  30648  satfun  33273  fundmpss  33646  dfon2lem6  33670  finminlem  34434  fvineqsneq  35510  pssexg  40127  xppss12  40130  psshepw  41285