Theorem strfv3

Description: Variant on strfv for large structures. (Contributed by Mario Carneiro, 10-Jan-2017)

	Ref	Expression
Hypotheses	strfv3.u	|- ( ph -> U = S )
	strfv3.s	|- S Struct X
	strfv3.e	|- E = Slot ( E ` ndx )
	strfv3.n	|- { <. ( E ` ndx ) , C >. } C_ S
	strfv3.c	|- ( ph -> C e. V )
	strfv3.a	|- A = ( E ` U )
Assertion	strfv3	|- ( ph -> A = C )

Proof

Step	Hyp	Ref	Expression
1		strfv3.u	|- ( ph -> U = S )
2		strfv3.s	|- S Struct X
3		strfv3.e	|- E = Slot ( E ` ndx )
4		strfv3.n	|- { <. ( E ` ndx ) , C >. } C_ S
5		strfv3.c	|- ( ph -> C e. V )
6		strfv3.a	|- A = ( E ` U )
7	2 3 4	strfv	|- ( C e. V -> C = ( E ` S ) )
8	5 7	syl	|- ( ph -> C = ( E ` S ) )
9	1	fveq2d	|- ( ph -> ( E ` U ) = ( E ` S ) )
10	8 9	eqtr4d	|- ( ph -> C = ( E ` U ) )
11	6 10	eqtr4id	|- ( ph -> A = C )