Theorem strfvnd

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

	Ref	Expression
Hypotheses	strfvnd.c	⊢ 𝐸 = Slot 𝑁
	strfvnd.f	⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
Assertion	strfvnd	⊢ ( 𝜑 → ( 𝐸 ‘ 𝑆 ) = ( 𝑆 ‘ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		strfvnd.c	⊢ 𝐸 = Slot 𝑁
2		strfvnd.f	⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
3		elex	⊢ ( 𝑆 ∈ 𝑉 → 𝑆 ∈ V )
4		fveq1	⊢ ( 𝑥 = 𝑆 → ( 𝑥 ‘ 𝑁 ) = ( 𝑆 ‘ 𝑁 ) )
5		df-slot	⊢ Slot 𝑁 = ( 𝑥 ∈ V ↦ ( 𝑥 ‘ 𝑁 ) )
6	1 5	eqtri	⊢ 𝐸 = ( 𝑥 ∈ V ↦ ( 𝑥 ‘ 𝑁 ) )
7		fvex	⊢ ( 𝑆 ‘ 𝑁 ) ∈ V
8	4 6 7	fvmpt	⊢ ( 𝑆 ∈ V → ( 𝐸 ‘ 𝑆 ) = ( 𝑆 ‘ 𝑁 ) )
9	2 3 8	3syl	⊢ ( 𝜑 → ( 𝐸 ‘ 𝑆 ) = ( 𝑆 ‘ 𝑁 ) )