Theorem pssss 4073

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

Syntax hints:   → wi 4   ≠ wne 2932   ⊆ wss 3926   ⊊ wpss 3927

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 207  df-an 396  df-pss 3946

This theorem is referenced by:  pssssd  4075  sspss  4077  pssn2lp  4079  psstr  4082  brrpssg  7719  pssnn  9182  php  9221  php2  9222  php3  9223  phpOLD  9231  php2OLD  9232  php3OLD  9233  findcard3  9290  findcard3OLD  9291  marypha1lem  9445  infpssr  10322  fin4en1  10323  ssfin4  10324  fin23lem34  10360  npex  11000  elnp  11001  suplem1pr  11066  lsmcv  21102  islbs3  21116  obslbs  21690  spansncvi  31633  chrelati  32345  atcvatlem  32366  satfun  35433  fundmpss  35784  dfon2lem6  35806  finminlem  36336  fvineqsneq  37430  pssexg  42277  xppss12  42280  psshepw  43812