Theorem pssss 4024

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

This proof depends on syntax axioms:   → wi 4   ≠ wne 2955   ⊆ wss 3896   ⊊ wpss 4012

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-pss 4013

This theorem is used by:  pssssd  4026  sspss  4028  pssn2lp  4031  psstr  4034  brrpssg  7743  pssnn  9189  php  9227  php2  9228  php3  9229  findcard3  9279  marypha1lem  9430  infpssr  10391  fin4en1  10392  ssfin4  10393  fin23lem34  10429  npex  11076  elnp  11077  suplem1pr  11142  lsmcv  21426  islbs3  21440  obslbs  22043  spansncvi  32261  chrelati  32973  atcvatlem  32994  satfun  36264  fundmpss  36626  dfon2lem6  36644  finminlem  37200  fvineqsneq  38442  pssexg  43387  xppss12  43390  psshepw  44895