Metamath Proof Explorer


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 }