Theorem pssss 1567

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

Assertion

Ref	Expression
pssss	|- (A (. B -> A (_ B)

Proof of Theorem pssss

Step	Hyp	Ref	Expression
1		df-pss 1494	. 2 |- (A (. B <-> (A (_ B /\ A =/= B))
2	1	pm3.26bd 259	1 |- (A (. B -> A (_ B)

Syntax hints:   -> wi 2   =/= wne 1190   (_ wss 1487   (. wpss 1488

This theorem is referenced by:  pssssd 1568  sspss 1569  psstr 1574  npss0 1731  php 3409  php2 3410  php3 3411  pssnn 3428  inf5 3472  npex 3885  elnp 3886  suplem1pr 3955  spansncv 5542  chrelat 5757  atcvatlem 5770

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

This theorem depends on definitions:  df-bi 128  df-an 198  df-pss 1494

metamath.org