Definition df-pss

Description: Define proper subclass (or strict subclass) relationship between two classes. Definition 5.9 of TakeutiZaring p. 17. For example, { 1 , 2 } C. { 1 , 2 , 3 } ( ex-pss ). Note that -. A C. A (proved in pssirr ). Contrast this relationship with the relationship A C_ B (as defined in df-ss ). Other possible definitions are given by dfpss2 and dfpss3 . (Contributed by NM, 7-Feb-1996)

	Ref	Expression
Assertion	df-pss	$$⊢A\subset B\leftrightarrow \left(A\subseteq B\wedge A\ne B\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1		cB	$$classB$$
2	0 1	wpss	$$wffA\subset B$$
3	0 1	wss	$$wffA\subseteq B$$
4	0 1	wne	$$wffA\ne B$$
5	3 4	wa	$$wff\left(A\subseteq B\wedge A\ne B\right)$$
6	2 5	wb	$$wff\left(A\subset B\leftrightarrow \left(A\subseteq B\wedge A\ne B\right)\right)$$