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

Definition df-concat 12544
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
Distinct variable group:   , ,

Detailed syntax breakdown of Definition df-concat
StepHypRef Expression
1 cconcat 12536 . 2
2 vs . . 3
3 vt . . 3
4 cvv 3109 . . 3
5 vx . . . 4
6 cc0 9513 . . . . 5
72cv 1394 . . . . . . 7
8 chash 12405 . . . . . . 7
97, 8cfv 5593 . . . . . 6
103cv 1394 . . . . . . 7
1110, 8cfv 5593 . . . . . 6
12 caddc 9516 . . . . . 6
139, 11, 12co 6296 . . . . 5
14 cfzo 11824 . . . . 5
156, 13, 14co 6296 . . . 4
165cv 1394 . . . . . 6
176, 9, 14co 6296 . . . . . 6
1816, 17wcel 1818 . . . . 5
1916, 7cfv 5593 . . . . 5
20 cmin 9828 . . . . . . 7
2116, 9, 20co 6296 . . . . . 6
2221, 10cfv 5593 . . . . 5
2318, 19, 22cif 3941 . . . 4
245, 15, 23cmpt 4510 . . 3
252, 3, 4, 4, 24cmpt2 6298 . 2
261, 25wceq 1395 1
Colors of variables: wff setvar class
This definition is referenced by:  ccatfn  12591  ccatfval  12592
  Copyright terms: Public domain W3C validator