Theorem pssss 2143

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

Syntax hints:   -> wi 3   =/= wne 1585   (_ wss 2047   (. wpss 2048

This theorem is referenced by:  pssssd 2144  sspss 2145  psstr 2150  npss0 2309  php 4513  php2 4514  php3 4515  php3OLD 4516  pssnn 4534  npex 5091  elnp 5092  suplem1pr 5161  spansncv 9597  chrelat 10291  atcvatlem 10312

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 2055

Copyright terms: Public domain