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	|- ( ph -> ( Base ` C ) = ( Base ` D ) )
	homfeqd.2	|- ( ph -> ( Hom ` C ) = ( Hom ` D ) )
Assertion	homfeqd	|- ( ph -> ( Homf ` C ) = ( Homf ` D ) )

Proof

Step	Hyp	Ref	Expression
1		homfeqd.1	|- ( ph -> ( Base ` C ) = ( Base ` D ) )
2		homfeqd.2	|- ( ph -> ( Hom ` C ) = ( Hom ` D ) )
3	2	oveqd	|- ( ph -> ( x ( Hom ` C ) y ) = ( x ( Hom ` D ) y ) )
4	3	ralrimivw	|- ( ph -> A. y e. ( Base ` C ) ( x ( Hom ` C ) y ) = ( x ( Hom ` D ) y ) )
5	4	ralrimivw	|- ( ph -> A. x e. ( Base ` C ) A. y e. ( Base ` C ) ( x ( Hom ` C ) y ) = ( x ( Hom ` D ) y ) )
6		eqid	|- ( Hom ` C ) = ( Hom ` C )
7		eqid	|- ( Hom ` D ) = ( Hom ` D )
8		eqidd	|- ( ph -> ( Base ` C ) = ( Base ` C ) )
9	6 7 8 1	homfeq	|- ( ph -> ( ( Homf ` C ) = ( Homf ` D ) <-> A. x e. ( Base ` C ) A. y e. ( Base ` C ) ( x ( Hom ` C ) y ) = ( x ( Hom ` D ) y ) ) )
10	5 9	mpbird	|- ( ph -> ( Homf ` C ) = ( Homf ` D ) )