# Metamath Proof Explorer

## Theorem fmpt

Description: Functionality of the mapping operation. (Contributed by Mario Carneiro, 26-Jul-2013) (Revised by Mario Carneiro, 31-Aug-2015)

Ref Expression
Hypothesis fmpt.1
`|- F = ( x e. A |-> C )`
Assertion fmpt
`|- ( A. x e. A C e. B <-> F : A --> B )`

### Proof

Step Hyp Ref Expression
1 fmpt.1
` |-  F = ( x e. A |-> C )`
2 1 fnmpt
` |-  ( A. x e. A C e. B -> F Fn A )`
3 1 rnmpt
` |-  ran F = { y | E. x e. A y = C }`
4 r19.29
` |-  ( ( A. x e. A C e. B /\ E. x e. A y = C ) -> E. x e. A ( C e. B /\ y = C ) )`
5 eleq1
` |-  ( y = C -> ( y e. B <-> C e. B ) )`
6 5 biimparc
` |-  ( ( C e. B /\ y = C ) -> y e. B )`
7 6 rexlimivw
` |-  ( E. x e. A ( C e. B /\ y = C ) -> y e. B )`
8 4 7 syl
` |-  ( ( A. x e. A C e. B /\ E. x e. A y = C ) -> y e. B )`
9 8 ex
` |-  ( A. x e. A C e. B -> ( E. x e. A y = C -> y e. B ) )`
10 9 abssdv
` |-  ( A. x e. A C e. B -> { y | E. x e. A y = C } C_ B )`
11 3 10 eqsstrid
` |-  ( A. x e. A C e. B -> ran F C_ B )`
12 df-f
` |-  ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )`
13 2 11 12 sylanbrc
` |-  ( A. x e. A C e. B -> F : A --> B )`
14 1 mptpreima
` |-  ( `' F " B ) = { x e. A | C e. B }`
15 fimacnv
` |-  ( F : A --> B -> ( `' F " B ) = A )`
16 14 15 syl5reqr
` |-  ( F : A --> B -> A = { x e. A | C e. B } )`
17 rabid2
` |-  ( A = { x e. A | C e. B } <-> A. x e. A C e. B )`
18 16 17 sylib
` |-  ( F : A --> B -> A. x e. A C e. B )`
19 13 18 impbii
` |-  ( A. x e. A C e. B <-> F : A --> B )`