Metamath Proof Explorer

Theorem mptfcl

Description: Interpret range of a maps-to notation as a constraint on the definition. (Contributed by Stefan O'Rear, 10-Oct-2014)

Ref Expression
Assertion mptfcl 
|- ( ( t e. A |-> B ) : A --> C -> ( t e. A -> B e. C ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( t e. A |-> B ) = ( t e. A |-> B )
2 1 fmpt 
 |-  ( A. t e. A B e. C <-> ( t e. A |-> B ) : A --> C )
3 rsp 
 |-  ( A. t e. A B e. C -> ( t e. A -> B e. C ) )
4 2 3 sylbir 
 |-  ( ( t e. A |-> B ) : A --> C -> ( t e. A -> B e. C ) )