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

Definition df-concat 11679
 Description: Define the concatenation operator which combines two words. (Contributed by FL, 14-Jan-2014.) (Revised by Stefan O'Rear, 15-Aug-2015.)
Assertion
Ref Expression
df-concat concat ..^ ..^
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-concat
StepHypRef Expression
1 cconcat 11673 . 2 concat
2 vs . . 3
3 vt . . 3
4 cvv 2916 . . 3
5 vx . . . 4
6 cc0 8946 . . . . 5
72cv 1648 . . . . . . 7
8 chash 11573 . . . . . . 7
97, 8cfv 5413 . . . . . 6
103cv 1648 . . . . . . 7
1110, 8cfv 5413 . . . . . 6
12 caddc 8949 . . . . . 6
139, 11, 12co 6040 . . . . 5
14 cfzo 11090 . . . . 5 ..^
156, 13, 14co 6040 . . . 4 ..^
165cv 1648 . . . . . 6
176, 9, 14co 6040 . . . . . 6 ..^
1816, 17wcel 1721 . . . . 5 ..^
1916, 7cfv 5413 . . . . 5
20 cmin 9247 . . . . . . 7
2116, 9, 20co 6040 . . . . . 6
2221, 10cfv 5413 . . . . 5
2318, 19, 22cif 3699 . . . 4 ..^
245, 15, 23cmpt 4226 . . 3 ..^ ..^
252, 3, 4, 4, 24cmpt2 6042 . 2 ..^ ..^
261, 25wceq 1649 1 concat ..^ ..^
 Colors of variables: wff set class This definition is referenced by:  ccatfn  11696  ccatfval  11697
 Copyright terms: Public domain W3C validator