Theorem pssss 2133

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 2045	. 2 |- (A (. B <-> (A (_ B /\ A =/= B))
2	1	pm3.26bi 322	1 |- (A (. B -> A (_ B)

Syntax hints:   -> wi 3   =/= wne 1577   (_ wss 2037   (. wpss 2038

This theorem is referenced by:  pssssd 2134  sspss 2135  psstr 2140  npss0 2299  php 4493  php2 4494  php3 4495  pssnn 4513  npex 5063  elnp 5064  suplem1pr 5133  spansncv 9514  chrelat 10199  atcvatlem 10220

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 147  df-an 225  df-pss 2045

Copyright terms: Public domain