Theorem strfv3

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

	Ref	Expression
Hypotheses	strfv3.u	$$⊢\phi \to U=S$$
	strfv3.s	$$⊢S\mathrm{Struct}X$$
	strfv3.e	$$⊢E=\mathrm{Slot}E\left(\mathrm{ndx}\right)$$
	strfv3.n	$$⊢\left\{⟨E\left(\mathrm{ndx}\right),C⟩\right\}\subseteq S$$
	strfv3.c	$$⊢\phi \to C\in V$$
	strfv3.a	$$⊢A=E\left(U\right)$$
Assertion	strfv3	$$⊢\phi \to A=C$$

Proof

Step	Hyp	Ref	Expression
1		strfv3.u	$$⊢\phi \to U=S$$
2		strfv3.s	$$⊢S\mathrm{Struct}X$$
3		strfv3.e	$$⊢E=\mathrm{Slot}E\left(\mathrm{ndx}\right)$$
4		strfv3.n	$$⊢\left\{⟨E\left(\mathrm{ndx}\right),C⟩\right\}\subseteq S$$
5		strfv3.c	$$⊢\phi \to C\in V$$
6		strfv3.a	$$⊢A=E\left(U\right)$$
7	2 3 4	strfv	$$⊢C\in V\to C=E\left(S\right)$$
8	5 7	syl	$$⊢\phi \to C=E\left(S\right)$$
9	1	fveq2d	$$⊢\phi \to E\left(U\right)=E\left(S\right)$$
10	8 9	eqtr4d	$$⊢\phi \to C=E\left(U\right)$$
11	6 10	eqtr4id	$$⊢\phi \to A=C$$