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

Definition df-cid 13886
 Description: Define the category identity arrow. Since it is uniquely defined when it exists, we do not need to add it to the data of the category, and instead extract it by uniqueness. (Contributed by Mario Carneiro, 3-Jan-2017.)
Assertion
Ref Expression
df-cid comp
Distinct variable group:   ,,,,,,,

Detailed syntax breakdown of Definition df-cid
StepHypRef Expression
1 ccid 13882 . 2
2 vc . . 3
3 ccat 13881 . . 3
4 vb . . . 4
52cv 1651 . . . . 5
6 cbs 13461 . . . . 5
75, 6cfv 5446 . . . 4
8 vh . . . . 5
9 chom 13532 . . . . . 6
105, 9cfv 5446 . . . . 5
11 vo . . . . . 6
12 cco 13533 . . . . . . 7 comp
135, 12cfv 5446 . . . . . 6 comp
14 vx . . . . . . 7
154cv 1651 . . . . . . 7
16 vg . . . . . . . . . . . . . 14
1716cv 1651 . . . . . . . . . . . . 13
18 vf . . . . . . . . . . . . . 14
1918cv 1651 . . . . . . . . . . . . 13
20 vy . . . . . . . . . . . . . . . 16
2120cv 1651 . . . . . . . . . . . . . . 15
2214cv 1651 . . . . . . . . . . . . . . 15
2321, 22cop 3809 . . . . . . . . . . . . . 14
2411cv 1651 . . . . . . . . . . . . . 14
2523, 22, 24co 6073 . . . . . . . . . . . . 13
2617, 19, 25co 6073 . . . . . . . . . . . 12
2726, 19wceq 1652 . . . . . . . . . . 11
288cv 1651 . . . . . . . . . . . 12
2921, 22, 28co 6073 . . . . . . . . . . 11
3027, 18, 29wral 2697 . . . . . . . . . 10
3122, 22cop 3809 . . . . . . . . . . . . . 14
3231, 21, 24co 6073 . . . . . . . . . . . . 13
3319, 17, 32co 6073 . . . . . . . . . . . 12
3433, 19wceq 1652 . . . . . . . . . . 11
3522, 21, 28co 6073 . . . . . . . . . . 11
3634, 18, 35wral 2697 . . . . . . . . . 10
3730, 36wa 359 . . . . . . . . 9
3837, 20, 15wral 2697 . . . . . . . 8
3922, 22, 28co 6073 . . . . . . . 8
4038, 16, 39crio 6534 . . . . . . 7
4114, 15, 40cmpt 4258 . . . . . 6
4211, 13, 41csb 3243 . . . . 5 comp
438, 10, 42csb 3243 . . . 4 comp
444, 7, 43csb 3243 . . 3 comp
452, 3, 44cmpt 4258 . 2 comp
461, 45wceq 1652 1 comp
 Colors of variables: wff set class This definition is referenced by:  cidfval  13893  cidffn  13895
 Copyright terms: Public domain W3C validator