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 } |
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 } |