# Metamath Proof Explorer

## Theorem catideu

Description: Each object in a category has a unique identity arrow. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Hypotheses catidex.b $⊢ B = Base C$
catidex.h $⊢ H = Hom ⁡ C$
catidex.o
catidex.c $⊢ φ → C ∈ Cat$
catidex.x $⊢ φ → X ∈ B$
Assertion catideu

### Proof

Step Hyp Ref Expression
1 catidex.b $⊢ B = Base C$
2 catidex.h $⊢ H = Hom ⁡ C$
3 catidex.o
4 catidex.c $⊢ φ → C ∈ Cat$
5 catidex.x $⊢ φ → X ∈ B$
6 1 2 3 4 5 catidex
7 oveq1 $⊢ y = X → y H X = X H X$
8 opeq1 $⊢ y = X → y X = X X$
9 8 oveq1d
10 9 oveqd
11 10 eqeq1d
12 7 11 raleqbidv
13 oveq2 $⊢ y = X → X H y = X H X$
14 oveq2
15 14 oveqd
16 15 eqeq1d
17 13 16 raleqbidv
18 12 17 anbi12d
19 18 rspcv
20 5 19 syl
21 20 ralrimivw
22 an3
23 oveq2
24 id $⊢ f = h → f = h$
25 23 24 eqeq12d
26 25 rspcv
27 oveq1
28 id $⊢ f = g → f = g$
29 27 28 eqeq12d
30 29 rspcv
31 26 30 im2anan9r
32 eqtr2
33 32 equcomd
34 22 31 33 syl56
35 34 rgen2
36 35 a1i
37 oveq1
38 37 eqeq1d
39 38 ralbidv
40 oveq2
41 40 eqeq1d
42 41 ralbidv
43 39 42 anbi12d
44 43 rmo4
45 36 44 sylibr
46 rmoim
47 21 45 46 sylc
48 reu5
49 6 47 48 sylanbrc