Theorem resshom

Description: Hom is unaffected by restriction. (Contributed by Mario Carneiro, 5-Jan-2017)

	Ref	Expression
Hypotheses	resshom.1	|- D = ( C |`s A )
	resshom.2	|- H = ( Hom ` C )
Assertion	resshom	|- ( A e. V -> H = ( Hom ` D ) )

Proof

Step	Hyp	Ref	Expression
1		resshom.1	|- D = ( C |`s A )
2		resshom.2	|- H = ( Hom ` C )
3		homid	|- Hom = Slot ( Hom ` ndx )
4		slotsbhcdif	|- ( ( Base ` ndx ) =/= ( Hom ` ndx ) /\ ( Base ` ndx ) =/= ( comp ` ndx ) /\ ( Hom ` ndx ) =/= ( comp ` ndx ) )
5		simp1	|- ( ( ( Base ` ndx ) =/= ( Hom ` ndx ) /\ ( Base ` ndx ) =/= ( comp ` ndx ) /\ ( Hom ` ndx ) =/= ( comp ` ndx ) ) -> ( Base ` ndx ) =/= ( Hom ` ndx ) )
6	5	necomd	|- ( ( ( Base ` ndx ) =/= ( Hom ` ndx ) /\ ( Base ` ndx ) =/= ( comp ` ndx ) /\ ( Hom ` ndx ) =/= ( comp ` ndx ) ) -> ( Hom ` ndx ) =/= ( Base ` ndx ) )
7	4 6	ax-mp	|- ( Hom ` ndx ) =/= ( Base ` ndx )
8	1 2 3 7	resseqnbas	|- ( A e. V -> H = ( Hom ` D ) )