Metamath Proof Explorer


Theorem fnmpt

Description: The maps-to notation defines a function with domain. (Contributed by NM, 9-Apr-2013)

Ref Expression
Hypothesis mptfng.1
|- F = ( x e. A |-> B )
Assertion fnmpt
|- ( A. x e. A B e. V -> F Fn A )

Proof

Step Hyp Ref Expression
1 mptfng.1
 |-  F = ( x e. A |-> B )
2 elex
 |-  ( B e. V -> B e. _V )
3 2 ralimi
 |-  ( A. x e. A B e. V -> A. x e. A B e. _V )
4 1 mptfng
 |-  ( A. x e. A B e. _V <-> F Fn A )
5 3 4 sylib
 |-  ( A. x e. A B e. V -> F Fn A )