Theorem strfvd

Description: Deduction version of strfv . (Contributed by Mario Carneiro, 15-Nov-2014)

	Ref	Expression
Hypotheses	strfvd.e	|- E = Slot ( E ` ndx )
	strfvd.s	|- ( ph -> S e. V )
	strfvd.f	|- ( ph -> Fun S )
	strfvd.n	|- ( ph -> <. ( E ` ndx ) , C >. e. S )
Assertion	strfvd	|- ( ph -> C = ( E ` S ) )

Proof

Step	Hyp	Ref	Expression
1		strfvd.e	|- E = Slot ( E ` ndx )
2		strfvd.s	|- ( ph -> S e. V )
3		strfvd.f	|- ( ph -> Fun S )
4		strfvd.n	|- ( ph -> <. ( E ` ndx ) , C >. e. S )
5	1 2	strfvnd	|- ( ph -> ( E ` S ) = ( S ` ( E ` ndx ) ) )
6		funopfv	|- ( Fun S -> ( <. ( E ` ndx ) , C >. e. S -> ( S ` ( E ` ndx ) ) = C ) )
7	3 4 6	sylc	|- ( ph -> ( S ` ( E ` ndx ) ) = C )
8	5 7	eqtr2d	|- ( ph -> C = ( E ` S ) )