Metamath Proof Explorer


Definition df-rcl

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 r*=xVz|xzIdomzranzz

Detailed syntax breakdown

Step Hyp Ref Expression
0 crcl classr*
1 vx setvarx
2 cvv classV
3 vz setvarz
4 1 cv setvarx
5 3 cv setvarz
6 4 5 wss wffxz
7 cid classI
8 5 cdm classdomz
9 5 crn classranz
10 8 9 cun classdomzranz
11 7 10 cres classIdomzranz
12 11 5 wss wffIdomzranzz
13 6 12 wa wffxzIdomzranzz
14 13 3 cab classz|xzIdomzranzz
15 14 cint classz|xzIdomzranzz
16 1 2 15 cmpt classxVz|xzIdomzranzz
17 0 16 wceq wffr*=xVz|xzIdomzranzz