Definition df-rpss

Description: Define a relation which corresponds to proper subsethood df-pss on sets. This allows 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	$$⊢[\subset ]=\left\{⟨x,y⟩|x\subset y\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crpss	$$class[\subset ]$$
1		vx	$$setvarx$$
2		vy	$$setvary$$
3	1	cv	$$setvarx$$
4	2	cv	$$setvary$$
5	3 4	wpss	$$wffx\subset y$$
6	5 1 2	copab	$$class\left\{⟨x,y⟩|x\subset y\right\}$$
7	0 6	wceq	$$wff[\subset ]=\left\{⟨x,y⟩|x\subset y\right\}$$