Theorem fmptf

Description: Functionality of the mapping operation. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	fmptf.1	|- F/_ x B
	fmptf.2	|- F = ( x e. A |-> C )
Assertion	fmptf	|- ( A. x e. A C e. B <-> F : A --> B )

Proof

Step	Hyp	Ref	Expression
1		fmptf.1	|- F/_ x B
2		fmptf.2	|- F = ( x e. A |-> C )
3		nfv	|- F/ y C e. B
4		nfcsb1v	|- F/_ x [_ y / x ]_ C
5	4 1	nfel	|- F/ x [_ y / x ]_ C e. B
6		csbeq1a	|- ( x = y -> C = [_ y / x ]_ C )
7	6	eleq1d	|- ( x = y -> ( C e. B <-> [_ y / x ]_ C e. B ) )
8	3 5 7	cbvralw	|- ( A. x e. A C e. B <-> A. y e. A [_ y / x ]_ C e. B )
9		nfcv	|- F/_ y C
10	9 4 6	cbvmpt	|- ( x e. A |-> C ) = ( y e. A |-> [_ y / x ]_ C )
11	2 10	eqtri	|- F = ( y e. A |-> [_ y / x ]_ C )
12	11	fmpt	|- ( A. y e. A [_ y / x ]_ C e. B <-> F : A --> B )
13	8 12	bitri	|- ( A. x e. A C e. B <-> F : A --> B )