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

Definition df-concat 11724
 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 11718 . 2 concat
2 vs . . 3
3 vt . . 3
4 cvv 2956 . . 3
5 vx . . . 4
6 cc0 8990 . . . . 5
72cv 1651 . . . . . . 7
8 chash 11618 . . . . . . 7
97, 8cfv 5454 . . . . . 6
103cv 1651 . . . . . . 7
1110, 8cfv 5454 . . . . . 6
12 caddc 8993 . . . . . 6
139, 11, 12co 6081 . . . . 5
14 cfzo 11135 . . . . 5 ..^
156, 13, 14co 6081 . . . 4 ..^
165cv 1651 . . . . . 6
176, 9, 14co 6081 . . . . . 6 ..^
1816, 17wcel 1725 . . . . 5 ..^
1916, 7cfv 5454 . . . . 5
20 cmin 9291 . . . . . . 7
2116, 9, 20co 6081 . . . . . 6
2221, 10cfv 5454 . . . . 5
2318, 19, 22cif 3739 . . . 4 ..^
245, 15, 23cmpt 4266 . . 3 ..^ ..^
252, 3, 4, 4, 24cmpt2 6083 . 2 ..^ ..^
261, 25wceq 1652 1 concat ..^ ..^
 Colors of variables: wff set class This definition is referenced by:  ccatfn  11741  ccatfval  11742
 Copyright terms: Public domain W3C validator