Theorem fnmptif

Description: Functionality and domain of an ordered-pair class abstraction. (Contributed by Glauco Siliprandi, 21-Dec-2024)

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

Proof

Step	Hyp	Ref	Expression
1		fnmptif.1	|- F/_ x A
2		fnmptif.2	|- B e. _V
3		fnmptif.3	|- F = ( x e. A |-> B )
4	2	rgenw	|- A. x e. A B e. _V
5	1	mptfnf	|- ( A. x e. A B e. _V <-> ( x e. A |-> B ) Fn A )
6	4 5	mpbi	|- ( x e. A |-> B ) Fn A
7	3	fneq1i	|- ( F Fn A <-> ( x e. A |-> B ) Fn A )
8	6 7	mpbir	|- F Fn A