Theorem pssss 4091

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

Syntax hints:   → wi 4   ≠ wne 2929   ⊆ wss 3944   ⊊ wpss 3945

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 206  df-an 395  df-pss 3964

This theorem is referenced by:  pssssd  4093  sspss  4095  pssn2lp  4097  psstr  4100  brrpssg  7731  pssnn  9196  php  9238  php2  9239  php3  9240  phpOLD  9250  php2OLD  9251  php3OLD  9252  pssnnOLD  9293  findcard3  9313  findcard3OLD  9314  marypha1lem  9463  infpssr  10338  fin4en1  10339  ssfin4  10340  fin23lem34  10376  npex  11016  elnp  11017  suplem1pr  11082  lsmcv  21046  islbs3  21060  obslbs  21686  spansncvi  31539  chrelati  32251  atcvatlem  32272  satfun  35154  fundmpss  35495  dfon2lem6  35517  finminlem  35935  fvineqsneq  37024  pssexg  41850  xppss12  41853  psshepw  43362