Definition df-rpss 6937

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

Assertion

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

Distinct variable group:   x, y

Detailed syntax breakdown of Definition df-rpss

Step	Hyp	Ref	Expression
1		crpss 6936	. 2 class [ C.]
2		vx	. . . . 5 setvar x
3	2	cv 1482	. . . 4 class x
4		vy	. . . . 5 setvar y
5	4	cv 1482	. . . 4 class y
6	3, 5	wpss 3575	. . 3 wff x C. y
7	6, 2, 4	copab 4712	. 2 class { <. x , y >. | x C. y }
8	1, 7	wceq 1483	1 wff [ C.] = { <. x , y >. | x C. y }

This definition is referenced by:  relrpss  6938  brrpssg  6939