Theorem strfv3

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

	Ref	Expression
Hypotheses	strfv3.u	⊢ ( 𝜑 → 𝑈 = 𝑆 )
	strfv3.s	⊢ 𝑆 Struct 𝑋
	strfv3.e	⊢ 𝐸 = Slot ( 𝐸 ‘ ndx )
	strfv3.n	⊢ { ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ } ⊆ 𝑆
	strfv3.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
	strfv3.a	⊢ 𝐴 = ( 𝐸 ‘ 𝑈 )
Assertion	strfv3	⊢ ( 𝜑 → 𝐴 = 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		strfv3.u	⊢ ( 𝜑 → 𝑈 = 𝑆 )
2		strfv3.s	⊢ 𝑆 Struct 𝑋
3		strfv3.e	⊢ 𝐸 = Slot ( 𝐸 ‘ ndx )
4		strfv3.n	⊢ { ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ } ⊆ 𝑆
5		strfv3.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
6		strfv3.a	⊢ 𝐴 = ( 𝐸 ‘ 𝑈 )
7	2 3 4	strfv	⊢ ( 𝐶 ∈ 𝑉 → 𝐶 = ( 𝐸 ‘ 𝑆 ) )
8	5 7	syl	⊢ ( 𝜑 → 𝐶 = ( 𝐸 ‘ 𝑆 ) )
9	1	fveq2d	⊢ ( 𝜑 → ( 𝐸 ‘ 𝑈 ) = ( 𝐸 ‘ 𝑆 ) )
10	8 9	eqtr4d	⊢ ( 𝜑 → 𝐶 = ( 𝐸 ‘ 𝑈 ) )
11	6 10	eqtr4id	⊢ ( 𝜑 → 𝐴 = 𝐶 )