Theorem pssss 2705

Description: A proper subclass is a subclass. Theorem 10 of [Suppes] p. 23.

Assertion

Ref	Expression
pssss	|- (A C. B -> A C_ B)

Proof of Theorem pssss

Step	Hyp	Ref	Expression
1		df-pss 2607	. 2 |- (A C. B <-> (A C_ B /\ A =/= B))
2	1	simplbi 349	1 |- (A C. B -> A C_ B)

Syntax hints:   -> wi 3   =/= wne 2017   C_ wss 2593   C. wpss 2594

This theorem is referenced by:  pssssd 2706  sspss 2707  pssn2lp 2709  psstr 2714  npss0OLD 2912  php 5607  php2 5608  php3 5609  pssnn 5628  npex 6243  elnp 6244  suplem1pr 6313  spansncvi 11232  chrelati 11936  atcvatlem 11957  fundmpss 13836  dfon2lem6 13854  dford4lem1 13859  finminlem 15367

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 164  df-an 242  df-pss 2607

Copyright terms: Public domain