Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-rtrcl Structured version   Unicode version

Definition df-rtrcl 21804
 Description: Reflexive-transitive closure of a relation. Experimental. (Contributed by FL, 27-Jun-2011.)
Assertion
Ref Expression
df-rtrcl
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-rtrcl
StepHypRef Expression
1 crtcl 21802 . 2
2 vx . . 3
3 cvv 2962 . . 3
4 cid 4522 . . . . . . . 8
52cv 1652 . . . . . . . . . 10
65cdm 4907 . . . . . . . . 9
75crn 4908 . . . . . . . . 9
86, 7cun 3304 . . . . . . . 8
94, 8cres 4909 . . . . . . 7
10 vz . . . . . . . 8
1110cv 1652 . . . . . . 7
129, 11wss 3306 . . . . . 6
135, 11wss 3306 . . . . . 6
1411, 11ccom 4911 . . . . . . 7
1514, 11wss 3306 . . . . . 6
1612, 13, 15w3a 937 . . . . 5
1716, 10cab 2428 . . . 4
1817cint 4074 . . 3
192, 3, 18cmpt 4291 . 2
201, 19wceq 1653 1
 Colors of variables: wff set class This definition is referenced by:  dfrtrcl2  25179
 Copyright terms: Public domain W3C validator