Theorem fmptff

Description: Functionality of the mapping operation. (Contributed by Glauco Siliprandi, 5-Jan-2025)

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

Proof

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