Definition df-rpss

Description: Define a relation which corresponds to proper subsethood df-pss on sets. This allows us to use proper subsethood with general concepts that require relations, such as strict ordering, see sorpss . (Contributed by Stefan O'Rear, 2-Nov-2014)

	Ref	Expression
Assertion	df-rpss	|- [C.] = { <. x , y >. | x C. y }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crpss	|- [C.]
1		vx	|- x
2		vy	|- y
3	1	cv	|- x
4	2	cv	|- y
5	3 4	wpss	|- x C. y
6	5 1 2	copab	|- { <. x , y >. | x C. y }
7	0 6	wceq	|- [C.] = { <. x , y >. | x C. y }