# Metamath Proof Explorer

## Theorem fmpt2d

Description: Domain and codomain of the mapping operation; deduction form. (Contributed by NM, 27-Dec-2014)

Ref Expression
Hypotheses fmpt2d.2
`|- ( ( ph /\ x e. A ) -> B e. V )`
fmpt2d.1
`|- ( ph -> F = ( x e. A |-> B ) )`
fmpt2d.3
`|- ( ( ph /\ y e. A ) -> ( F ` y ) e. C )`
Assertion fmpt2d
`|- ( ph -> F : A --> C )`

### Proof

Step Hyp Ref Expression
1 fmpt2d.2
` |-  ( ( ph /\ x e. A ) -> B e. V )`
2 fmpt2d.1
` |-  ( ph -> F = ( x e. A |-> B ) )`
3 fmpt2d.3
` |-  ( ( ph /\ y e. A ) -> ( F ` y ) e. C )`
4 1 ralrimiva
` |-  ( ph -> A. x e. A B e. V )`
5 eqid
` |-  ( x e. A |-> B ) = ( x e. A |-> B )`
6 5 fnmpt
` |-  ( A. x e. A B e. V -> ( x e. A |-> B ) Fn A )`
7 4 6 syl
` |-  ( ph -> ( x e. A |-> B ) Fn A )`
8 2 fneq1d
` |-  ( ph -> ( F Fn A <-> ( x e. A |-> B ) Fn A ) )`
9 7 8 mpbird
` |-  ( ph -> F Fn A )`
10 3 ralrimiva
` |-  ( ph -> A. y e. A ( F ` y ) e. C )`
11 ffnfv
` |-  ( F : A --> C <-> ( F Fn A /\ A. y e. A ( F ` y ) e. C ) )`
12 9 10 11 sylanbrc
` |-  ( ph -> F : A --> C )`