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

Definition df-efg 17371
 Description: Define the free group equivalence relation, which is the smallest equivalence relation such that for any words and formal symbol with inverse , . (Contributed by Mario Carneiro, 1-Oct-2015.)
Assertion
Ref Expression
df-efg ~FG Word Word splice
Distinct variable group:   ,,,,,

Detailed syntax breakdown of Definition df-efg
StepHypRef Expression
1 cefg 17368 . 2 ~FG
2 vi . . 3
3 cvv 3047 . . 3
42cv 1445 . . . . . . . . 9
5 c2o 7181 . . . . . . . . 9
64, 5cxp 4835 . . . . . . . 8
76cword 12663 . . . . . . 7 Word
8 vr . . . . . . . 8
98cv 1445 . . . . . . 7
107, 9wer 7365 . . . . . 6 Word
11 vx . . . . . . . . . . . 12
1211cv 1445 . . . . . . . . . . 11
13 vn . . . . . . . . . . . . . 14
1413cv 1445 . . . . . . . . . . . . 13
15 vy . . . . . . . . . . . . . . . 16
1615cv 1445 . . . . . . . . . . . . . . 15
17 vz . . . . . . . . . . . . . . . 16
1817cv 1445 . . . . . . . . . . . . . . 15
1916, 18cop 3976 . . . . . . . . . . . . . 14
20 c1o 7180 . . . . . . . . . . . . . . . 16
2120, 18cdif 3403 . . . . . . . . . . . . . . 15
2216, 21cop 3976 . . . . . . . . . . . . . 14
2319, 22cs2 12944 . . . . . . . . . . . . 13
2414, 14, 23cotp 3978 . . . . . . . . . . . 12
25 csplice 12668 . . . . . . . . . . . 12 splice
2612, 24, 25co 6295 . . . . . . . . . . 11 splice
2712, 26, 9wbr 4405 . . . . . . . . . 10 splice
2827, 17, 5wral 2739 . . . . . . . . 9 splice
2928, 15, 4wral 2739 . . . . . . . 8 splice
30 cc0 9544 . . . . . . . . 9
31 chash 12522 . . . . . . . . . 10
3212, 31cfv 5585 . . . . . . . . 9
33 cfz 11791 . . . . . . . . 9
3430, 32, 33co 6295 . . . . . . . 8
3529, 13, 34wral 2739 . . . . . . 7 splice
3635, 11, 7wral 2739 . . . . . 6 Word splice
3710, 36wa 371 . . . . 5 Word Word splice
3837, 8cab 2439 . . . 4 Word Word splice
3938cint 4237 . . 3 Word Word splice
402, 3, 39cmpt 4464 . 2 Word Word splice
411, 40wceq 1446 1 ~FG Word Word splice
 Colors of variables: wff setvar class This definition is referenced by:  efgval  17379
 Copyright terms: Public domain W3C validator