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 2956   ⊆ 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  7739  pssnn  9177  php  9215  php2  9216  php3  9217  findcard3  9267  marypha1lem  9418  infpssr  10379  fin4en1  10380  ssfin4  10381  fin23lem34  10417  npex  11064  elnp  11065  suplem1pr  11130  lsmcv  21412  islbs3  21426  obslbs  22029  spansncvi  32247  chrelati  32959  atcvatlem  32980  satfun  36155  fundmpss  36511  dfon2lem6  36530  finminlem  37086  fvineqsneq  38315  pssexg  43260  xppss12  43263  psshepw  44773