Theorem fnmpti

Description: Functionality and domain of an ordered-pair class abstraction. (Contributed by NM, 29-Jan-2004) (Revised by Mario Carneiro, 31-Aug-2015)

	Ref	Expression
Hypotheses	fnmpti.1	|- B e. _V
	fnmpti.2	|- F = ( x e. A |-> B )
Assertion	fnmpti	|- F Fn A

Proof

Step	Hyp	Ref	Expression
1		fnmpti.1	|- B e. _V
2		fnmpti.2	|- F = ( x e. A |-> B )
3	1	rgenw	|- A. x e. A B e. _V
4	2	mptfng	|- ( A. x e. A B e. _V <-> F Fn A )
5	3 4	mpbi	|- F Fn A