This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem homfeqd

Description: If two structures have the same Hom slot, they have the same Hom-sets. (Contributed by Mario Carneiro, 4-Jan-2017)

Ref Expression
Hypotheses homfeqd.1 ⊢ φ → Base C = Base D
homfeqd.2 ⊢ φ → Hom ⁡ C = Hom ⁡ D
Assertion homfeqd ⊢ φ → Hom 𝑓 ⁡ C = Hom 𝑓 ⁡ D

Proof

Step Hyp Ref Expression
1 homfeqd.1 ⊢ φ → Base C = Base D
2 homfeqd.2 ⊢ φ → Hom ⁡ C = Hom ⁡ D
3 2 oveqd ⊢ φ → x Hom ⁡ C y = x Hom ⁡ D y
4 3 ralrimivw ⊢ φ → ∀ y ∈ Base C x Hom ⁡ C y = x Hom ⁡ D y
5 4 ralrimivw ⊢ φ → ∀ x ∈ Base C ∀ y ∈ Base C x Hom ⁡ C y = x Hom ⁡ D y
6 eqid ⊢ Hom ⁡ C = Hom ⁡ C
7 eqid ⊢ Hom ⁡ D = Hom ⁡ D
8 eqidd ⊢ φ → Base C = Base C
9 6 7 8 1 homfeq ⊢ φ → Hom 𝑓 ⁡ C = Hom 𝑓 ⁡ D ↔ ∀ x ∈ Base C ∀ y ∈ Base C x Hom ⁡ C y = x Hom ⁡ D y
10 5 9 mpbird ⊢ φ → Hom 𝑓 ⁡ C = Hom 𝑓 ⁡ D