Mathbox for Drahflow < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-relexp Structured version   Unicode version

Definition df-relexp 25128
 Description: Definition of repeated composition of a relation with itself, aka relation exponentiation. (Contributed by Drahflow, 12-Nov-2015.)
Assertion
Ref Expression
df-relexp
Distinct variable group:   ,,,,

Detailed syntax breakdown of Definition df-relexp
StepHypRef Expression
1 crelexp 25127 . 2
2 vr . . 3
3 vn . . 3
4 cvv 2956 . . 3
5 cn0 10221 . . 3
63cv 1651 . . . 4
7 vx . . . . . 6
8 vy . . . . . 6
97cv 1651 . . . . . . 7
102cv 1651 . . . . . . 7
119, 10ccom 4882 . . . . . 6
127, 8, 4, 4, 11cmpt2 6083 . . . . 5
13 vz . . . . . 6
14 cid 4493 . . . . . . 7
1510cuni 4015 . . . . . . . 8
1615cuni 4015 . . . . . . 7
1714, 16cres 4880 . . . . . 6
1813, 4, 17cmpt 4266 . . . . 5
19 cc0 8990 . . . . 5
2012, 18, 19cseq 11323 . . . 4
216, 20cfv 5454 . . 3
222, 3, 4, 5, 21cmpt2 6083 . 2
231, 22wceq 1652 1
 Colors of variables: wff set class This definition is referenced by:  relexp0  25129  relexpsucr  25130
 Copyright terms: Public domain W3C validator