Theorem pssss 4030

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

Syntax hints:   → wi 4   ≠ wne 2943   ⊆ wss 3887   ⊊ wpss 3888

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 397  df-pss 3906

This theorem is referenced by:  pssssd  4032  sspss  4034  pssn2lp  4036  psstr  4039  brrpssg  7578  pssnn  8951  php  8993  php2  8994  php3  8995  phpOLD  9005  php2OLD  9006  php3OLD  9007  pssnnOLD  9040  findcard3  9057  marypha1lem  9192  infpssr  10064  fin4en1  10065  ssfin4  10066  fin23lem34  10102  npex  10742  elnp  10743  suplem1pr  10808  lsmcv  20403  islbs3  20417  obslbs  20937  spansncvi  30014  chrelati  30726  atcvatlem  30747  satfun  33373  fundmpss  33740  dfon2lem6  33764  finminlem  34507  fvineqsneq  35583  pssexg  40201  xppss12  40204  psshepw  41396