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 
|- ( 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 ) )