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

Definition df-efg 15333
 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 15330 . 2 ~FG
2 vi . . 3
3 cvv 2948 . . 3
42cv 1651 . . . . . . . . 9
5 c2o 6710 . . . . . . . . 9
64, 5cxp 4868 . . . . . . . 8
76cword 11709 . . . . . . 7 Word
8 vr . . . . . . . 8
98cv 1651 . . . . . . 7
107, 9wer 6894 . . . . . 6 Word
11 vx . . . . . . . . . . . 12
1211cv 1651 . . . . . . . . . . 11
13 vn . . . . . . . . . . . . . 14
1413cv 1651 . . . . . . . . . . . . 13
15 vy . . . . . . . . . . . . . . . 16
1615cv 1651 . . . . . . . . . . . . . . 15
17 vz . . . . . . . . . . . . . . . 16
1817cv 1651 . . . . . . . . . . . . . . 15
1916, 18cop 3809 . . . . . . . . . . . . . 14
20 c1o 6709 . . . . . . . . . . . . . . . 16
2120, 18cdif 3309 . . . . . . . . . . . . . . 15
2216, 21cop 3809 . . . . . . . . . . . . . 14
2319, 22cs2 11797 . . . . . . . . . . . . 13
2414, 14, 23cotp 3810 . . . . . . . . . . . 12
25 csplice 11713 . . . . . . . . . . . 12 splice
2612, 24, 25co 6073 . . . . . . . . . . 11 splice
2712, 26, 9wbr 4204 . . . . . . . . . 10 splice
2827, 17, 5wral 2697 . . . . . . . . 9 splice
2928, 15, 4wral 2697 . . . . . . . 8 splice
30 cc0 8982 . . . . . . . . 9
31 chash 11610 . . . . . . . . . 10
3212, 31cfv 5446 . . . . . . . . 9
33 cfz 11035 . . . . . . . . 9
3430, 32, 33co 6073 . . . . . . . 8
3529, 13, 34wral 2697 . . . . . . 7 splice
3635, 11, 7wral 2697 . . . . . 6 Word splice
3710, 36wa 359 . . . . 5 Word Word splice
3837, 8cab 2421 . . . 4 Word Word splice
3938cint 4042 . . 3 Word Word splice
402, 3, 39cmpt 4258 . 2 Word Word splice
411, 40wceq 1652 1 ~FG Word Word splice
 Colors of variables: wff set class This definition is referenced by:  efgval  15341
 Copyright terms: Public domain W3C validator