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 C. B <-> ( A C_ B /\ A =/= B ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	|- A
1		cB	|- B
2	0 1	wpss	|- A C. B
3	0 1	wss	|- A C_ B
4	0 1	wne	|- A =/= B
5	3 4	wa	|- ( A C_ B /\ A =/= B )
6	2 5	wb	|- ( A C. B <-> ( A C_ B /\ A =/= B ) )