Theorem strfvd

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

	Ref	Expression
Hypotheses	strfvd.e	⊢ 𝐸 = Slot ( 𝐸 ‘ ndx )
	strfvd.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
	strfvd.f	⊢ ( 𝜑 → Fun 𝑆 )
	strfvd.n	⊢ ( 𝜑 → ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ ∈ 𝑆 )
Assertion	strfvd	⊢ ( 𝜑 → 𝐶 = ( 𝐸 ‘ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		strfvd.e	⊢ 𝐸 = Slot ( 𝐸 ‘ ndx )
2		strfvd.s	⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
3		strfvd.f	⊢ ( 𝜑 → Fun 𝑆 )
4		strfvd.n	⊢ ( 𝜑 → ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ ∈ 𝑆 )
5	1 2	strfvnd	⊢ ( 𝜑 → ( 𝐸 ‘ 𝑆 ) = ( 𝑆 ‘ ( 𝐸 ‘ ndx ) ) )
6		funopfv	⊢ ( Fun 𝑆 → ( ⟨ ( 𝐸 ‘ ndx ) , 𝐶 ⟩ ∈ 𝑆 → ( 𝑆 ‘ ( 𝐸 ‘ ndx ) ) = 𝐶 ) )
7	3 4 6	sylc	⊢ ( 𝜑 → ( 𝑆 ‘ ( 𝐸 ‘ ndx ) ) = 𝐶 )
8	5 7	eqtr2d	⊢ ( 𝜑 → 𝐶 = ( 𝐸 ‘ 𝑆 ) )