Theorem mptfng

Description: The maps-to notation defines a function with domain. (Contributed by Scott Fenton, 21-Mar-2011)

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

Proof

Step	Hyp	Ref	Expression
1		mptfng.1	|- F = ( x e. A |-> B )
2		eueq	|- ( B e. _V <-> E! y y = B )
3	2	ralbii	|- ( A. x e. A B e. _V <-> A. x e. A E! y y = B )
4		df-mpt	|- ( x e. A |-> B ) = { <. x , y >. | ( x e. A /\ y = B ) }
5	1 4	eqtri	|- F = { <. x , y >. | ( x e. A /\ y = B ) }
6	5	fnopabg	|- ( A. x e. A E! y y = B <-> F Fn A )
7	3 6	bitri	|- ( A. x e. A B e. _V <-> F Fn A )