Theorem pssss 4028

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

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

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 4017

This theorem is used by:  pssssd  4030  sspss  4032  pssn2lp  4035  psstr  4038  brrpssg  7773  pssnn  9222  php  9260  php2  9261  php3  9262  findcard3  9312  marypha1lem  9462  infpssr  10425  fin4en1  10426  ssfin4  10427  fin23lem34  10463  npex  11110  elnp  11111  suplem1pr  11176  lsmcv  21470  islbs3  21484  obslbs  22091  spansncvi  32311  chrelati  33023  atcvatlem  33044  satfun  36384  elpssmo  36673  fundmpss  36747  dfon2lem6  36765  finminlem  37321  fvineqsneq  38603  pssexg  43547  xppss12  43550  psshepw  45049