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 ) ) |
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 ) ) |