Description: Reflexive closure of a relation. This is the smallest superset which has the reflexive property. (Contributed by RP, 5-Jun-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | df-rcl | |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | crcl | |
|
1 | vx | |
|
2 | cvv | |
|
3 | vz | |
|
4 | 1 | cv | |
5 | 3 | cv | |
6 | 4 5 | wss | |
7 | cid | |
|
8 | 5 | cdm | |
9 | 5 | crn | |
10 | 8 9 | cun | |
11 | 7 10 | cres | |
12 | 11 5 | wss | |
13 | 6 12 | wa | |
14 | 13 3 | cab | |
15 | 14 | cint | |
16 | 1 2 15 | cmpt | |
17 | 0 16 | wceq | |