Theorem pssss 4049

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

Syntax hints:   → wi 4   ≠ wne 2925   ⊆ wss 3903   ⊊ wpss 3904

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 3923

This theorem is referenced by:  pssssd  4051  sspss  4053  pssn2lp  4055  psstr  4058  brrpssg  7661  pssnn  9082  php  9121  php2  9122  php3  9123  findcard3  9172  marypha1lem  9323  infpssr  10202  fin4en1  10203  ssfin4  10204  fin23lem34  10240  npex  10880  elnp  10881  suplem1pr  10946  lsmcv  21048  islbs3  21062  obslbs  21637  spansncvi  31596  chrelati  32308  atcvatlem  32329  satfun  35384  fundmpss  35740  dfon2lem6  35762  finminlem  36292  fvineqsneq  37386  pssexg  42199  xppss12  42202  psshepw  43761