Metamath Proof Explorer


Theorem strfvnd

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

Ref Expression
Hypotheses strfvnd.c
|- E = Slot N
strfvnd.f
|- ( ph -> S e. V )
Assertion strfvnd
|- ( ph -> ( E ` S ) = ( S ` N ) )

Proof

Step Hyp Ref Expression
1 strfvnd.c
 |-  E = Slot N
2 strfvnd.f
 |-  ( ph -> S e. V )
3 elex
 |-  ( S e. V -> S e. _V )
4 fveq1
 |-  ( x = S -> ( x ` N ) = ( S ` N ) )
5 df-slot
 |-  Slot N = ( x e. _V |-> ( x ` N ) )
6 1 5 eqtri
 |-  E = ( x e. _V |-> ( x ` N ) )
7 fvex
 |-  ( S ` N ) e. _V
8 4 6 7 fvmpt
 |-  ( S e. _V -> ( E ` S ) = ( S ` N ) )
9 2 3 8 3syl
 |-  ( ph -> ( E ` S ) = ( S ` N ) )