Description: Value of a function given by the maps-to notation. Deduction version. (Contributed by Glauco Siliprandi, 11-Dec-2019)
Ref | Expression | ||
---|---|---|---|
Hypothesis | fvmpt2bd.1 | |- ( ph -> F = ( x e. A |-> B ) ) |
|
Assertion | fvmpt2bd | |- ( ( ph /\ x e. A /\ B e. C ) -> ( F ` x ) = B ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fvmpt2bd.1 | |- ( ph -> F = ( x e. A |-> B ) ) |
|
2 | 1 | fveq1d | |- ( ph -> ( F ` x ) = ( ( x e. A |-> B ) ` x ) ) |
3 | 2 | 3ad2ant1 | |- ( ( ph /\ x e. A /\ B e. C ) -> ( F ` x ) = ( ( x e. A |-> B ) ` x ) ) |
4 | eqid | |- ( x e. A |-> B ) = ( x e. A |-> B ) |
|
5 | 4 | fvmpt2 | |- ( ( x e. A /\ B e. C ) -> ( ( x e. A |-> B ) ` x ) = B ) |
6 | 5 | 3adant1 | |- ( ( ph /\ x e. A /\ B e. C ) -> ( ( x e. A |-> B ) ` x ) = B ) |
7 | 3 6 | eqtrd | |- ( ( ph /\ x e. A /\ B e. C ) -> ( F ` x ) = B ) |