Theorem funmpt

Description: A function in maps-to notation is a function. (Contributed by Mario Carneiro, 13-Jan-2013)

	Ref	Expression
Assertion	funmpt	|- Fun ( x e. A |-> B )

Proof

Step	Hyp	Ref	Expression
1		funopab4	|- Fun { <. x , y >. | ( x e. A /\ y = B ) }
2		df-mpt	|- ( x e. A |-> B ) = { <. x , y >. | ( x e. A /\ y = B ) }
3	2	funeqi	|- ( Fun ( x e. A |-> B ) <-> Fun { <. x , y >. | ( x e. A /\ y = B ) } )
4	1 3	mpbir	|- Fun ( x e. A |-> B )