Theorem pssss 4046

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

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

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 3919

This theorem is used by:  pssssd  4048  sspss  4050  pssn2lp  4053  psstr  4056  brrpssg  7726  pssnn  9163  php  9201  php2  9202  php3  9203  findcard3  9253  marypha1lem  9403  infpssr  10310  fin4en1  10311  ssfin4  10312  fin23lem34  10348  npex  10995  elnp  10996  suplem1pr  11061  lsmcv  21328  islbs3  21342  obslbs  21943  spansncvi  32133  chrelati  32845  atcvatlem  32866  satfun  35990  fundmpss  36346  dfon2lem6  36365  finminlem  36937  fvineqsneq  38166  pssexg  43096  xppss12  43099  psshepw  44628