Theorem pssss 4094

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

Syntax hints:   → wi 4   ≠ wne 2940   ⊆ wss 3947   ⊊ wpss 3948

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 397  df-pss 3966

This theorem is referenced by:  pssssd  4096  sspss  4098  pssn2lp  4100  psstr  4103  brrpssg  7711  pssnn  9164  php  9206  php2  9207  php3  9208  phpOLD  9218  php2OLD  9219  php3OLD  9220  pssnnOLD  9261  findcard3  9281  findcard3OLD  9282  marypha1lem  9424  infpssr  10299  fin4en1  10300  ssfin4  10301  fin23lem34  10337  npex  10977  elnp  10978  suplem1pr  11043  lsmcv  20746  islbs3  20760  obslbs  21276  spansncvi  30892  chrelati  31604  atcvatlem  31625  satfun  34390  fundmpss  34726  dfon2lem6  34748  finminlem  35191  fvineqsneq  36281  pssexg  41040  xppss12  41043  psshepw  42524