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	$$⊢\phi \to {\mathrm{Base}}_C={\mathrm{Base}}_D$$
	homfeqd.2	$$⊢\phi \to \mathrm{Hom}\left(C\right)=\mathrm{Hom}\left(D\right)$$
Assertion	homfeqd	$$⊢\phi \to {\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(D\right)$$

Proof

Step	Hyp	Ref	Expression
1		homfeqd.1	$$⊢\phi \to {\mathrm{Base}}_C={\mathrm{Base}}_D$$
2		homfeqd.2	$$⊢\phi \to \mathrm{Hom}\left(C\right)=\mathrm{Hom}\left(D\right)$$
3	2	oveqd	$$⊢\phi \to x\mathrm{Hom}\left(C\right)y=x\mathrm{Hom}\left(D\right)y$$
4	3	ralrimivw	$$⊢\phi \to \forall y\in {\mathrm{Base}}_{C}x\mathrm{Hom}\left(C\right)y=x\mathrm{Hom}\left(D\right)y$$
5	4	ralrimivw	$$⊢\phi \to \forall x\in {\mathrm{Base}}_C\forall y\in {\mathrm{Base}}_{C}x\mathrm{Hom}\left(C\right)y=x\mathrm{Hom}\left(D\right)y$$
6		eqid	$$⊢\mathrm{Hom}\left(C\right)=\mathrm{Hom}\left(C\right)$$
7		eqid	$$⊢\mathrm{Hom}\left(D\right)=\mathrm{Hom}\left(D\right)$$
8		eqidd	$$⊢\phi \to {\mathrm{Base}}_C={\mathrm{Base}}_C$$
9	6 7 8 1	homfeq	$$⊢\phi \to \left({\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(D\right)\leftrightarrow \forall x\in {\mathrm{Base}}_C\forall y\in {\mathrm{Base}}_{C}x\mathrm{Hom}\left(C\right)y=x\mathrm{Hom}\left(D\right)y\right)$$
10	5 9	mpbird	$$⊢\phi \to {\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(D\right)$$