Theorem fmptdF

Description: Domain and codomain of the mapping operation; deduction form. This version of fmptd uses bound-variable hypothesis instead of distinct variable conditions. (Contributed by Thierry Arnoux, 28-Mar-2017)

	Ref	Expression
Hypotheses	fmptdF.p	|- F/ x ph
	fmptdF.a	|- F/_ x A
	fmptdF.c	|- F/_ x C
	fmptdF.1	|- ( ( ph /\ x e. A ) -> B e. C )
	fmptdF.2	|- F = ( x e. A |-> B )
Assertion	fmptdF	|- ( ph -> F : A --> C )

Proof

Step	Hyp	Ref	Expression
1		fmptdF.p	|- F/ x ph
2		fmptdF.a	|- F/_ x A
3		fmptdF.c	|- F/_ x C
4		fmptdF.1	|- ( ( ph /\ x e. A ) -> B e. C )
5		fmptdF.2	|- F = ( x e. A |-> B )
6	4	sbimi	|- ( [ y / x ] ( ph /\ x e. A ) -> [ y / x ] B e. C )
7		sban	|- ( [ y / x ] ( ph /\ x e. A ) <-> ( [ y / x ] ph /\ [ y / x ] x e. A ) )
8	1	sbf	|- ( [ y / x ] ph <-> ph )
9	2	clelsb1fw	|- ( [ y / x ] x e. A <-> y e. A )
10	8 9	anbi12i	|- ( ( [ y / x ] ph /\ [ y / x ] x e. A ) <-> ( ph /\ y e. A ) )
11	7 10	bitri	|- ( [ y / x ] ( ph /\ x e. A ) <-> ( ph /\ y e. A ) )
12		sbsbc	|- ( [ y / x ] B e. C <-> [. y / x ]. B e. C )
13		sbcel12	|- ( [. y / x ]. B e. C <-> [_ y / x ]_ B e. [_ y / x ]_ C )
14		vex	|- y e. _V
15	14 3	csbgfi	|- [_ y / x ]_ C = C
16	15	eleq2i	|- ( [_ y / x ]_ B e. [_ y / x ]_ C <-> [_ y / x ]_ B e. C )
17	13 16	bitri	|- ( [. y / x ]. B e. C <-> [_ y / x ]_ B e. C )
18	12 17	bitri	|- ( [ y / x ] B e. C <-> [_ y / x ]_ B e. C )
19	6 11 18	3imtr3i	|- ( ( ph /\ y e. A ) -> [_ y / x ]_ B e. C )
20	19	ralrimiva	|- ( ph -> A. y e. A [_ y / x ]_ B e. C )
21		nfcv	|- F/_ y A
22		nfcv	|- F/_ y B
23		nfcsb1v	|- F/_ x [_ y / x ]_ B
24		csbeq1a	|- ( x = y -> B = [_ y / x ]_ B )
25	2 21 22 23 24	cbvmptf	|- ( x e. A |-> B ) = ( y e. A |-> [_ y / x ]_ B )
26	25	fmpt	|- ( A. y e. A [_ y / x ]_ B e. C <-> ( x e. A |-> B ) : A --> C )
27	20 26	sylib	|- ( ph -> ( x e. A |-> B ) : A --> C )
28	5	feq1i	|- ( F : A --> C <-> ( x e. A |-> B ) : A --> C )
29	27 28	sylibr	|- ( ph -> F : A --> C )