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	$$⊢Ⅎx\phi$$
	fmptdF.a	$$⊢\underset{\_}{Ⅎ}xA$$
	fmptdF.c	$$⊢\underset{\_}{Ⅎ}xC$$
	fmptdF.1	$$⊢\left(\phi \wedge x\in A\right)\to B\in C$$
	fmptdF.2	$$⊢F=\left(x\in A⟼B\right)$$
Assertion	fmptdF	$$⊢\phi \to F:A⟶C$$

Proof

Step	Hyp	Ref	Expression
1		fmptdF.p	$$⊢Ⅎx\phi$$
2		fmptdF.a	$$⊢\underset{\_}{Ⅎ}xA$$
3		fmptdF.c	$$⊢\underset{\_}{Ⅎ}xC$$
4		fmptdF.1	$$⊢\left(\phi \wedge x\in A\right)\to B\in C$$
5		fmptdF.2	$$⊢F=\left(x\in A⟼B\right)$$
6	4	sbimi	$$⊢\left[y/x\right]\left(\phi \wedge x\in A\right)\to \left[y/x\right]B\in C$$
7		sban	$$⊢\left[y/x\right]\left(\phi \wedge x\in A\right)\leftrightarrow \left(\left[y/x\right]\phi \wedge \left[y/x\right]x\in A\right)$$
8	1	sbf	$$⊢\left[y/x\right]\phi \leftrightarrow \phi$$
9	2	clelsb1fw	$$⊢\left[y/x\right]x\in A\leftrightarrow y\in A$$
10	8 9	anbi12i	$$⊢\left(\left[y/x\right]\phi \wedge \left[y/x\right]x\in A\right)\leftrightarrow \left(\phi \wedge y\in A\right)$$
11	7 10	bitri	$$⊢\left[y/x\right]\left(\phi \wedge x\in A\right)\leftrightarrow \left(\phi \wedge y\in A\right)$$
12		sbsbc	$$⊢\left[y/x\right]B\in C\leftrightarrow \underset{\dot{}}{[}y/x\underset{\dot{}}{]}B\in C$$
13		sbcel12	$$⊢\underset{\dot{}}{[}y/x\underset{\dot{}}{]}B\in C\leftrightarrow ⦋y/x⦌B\in ⦋y/x⦌C$$
14		vex	$$⊢y\in \mathrm{V}$$
15	14 3	csbgfi	$$⊢⦋y/x⦌C=C$$
16	15	eleq2i	$$⊢⦋y/x⦌B\in ⦋y/x⦌C\leftrightarrow ⦋y/x⦌B\in C$$
17	13 16	bitri	$$⊢\underset{\dot{}}{[}y/x\underset{\dot{}}{]}B\in C\leftrightarrow ⦋y/x⦌B\in C$$
18	12 17	bitri	$$⊢\left[y/x\right]B\in C\leftrightarrow ⦋y/x⦌B\in C$$
19	6 11 18	3imtr3i	$$⊢\left(\phi \wedge y\in A\right)\to ⦋y/x⦌B\in C$$
20	19	ralrimiva	$$⊢\phi \to \forall y\in A⦋y/x⦌B\in C$$
21		nfcv	$$⊢\underset{\_}{Ⅎ}yA$$
22		nfcv	$$⊢\underset{\_}{Ⅎ}yB$$
23		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋y/x⦌B$$
24		csbeq1a	$$⊢x=y\to B=⦋y/x⦌B$$
25	2 21 22 23 24	cbvmptf	$$⊢\left(x\in A⟼B\right)=\left(y\in A⟼⦋y/x⦌B\right)$$
26	25	fmpt	$$⊢\forall y\in A⦋y/x⦌B\in C\leftrightarrow \left(x\in A⟼B\right):A⟶C$$
27	20 26	sylib	$$⊢\phi \to \left(x\in A⟼B\right):A⟶C$$
28	5	feq1i	$$⊢F:A⟶C\leftrightarrow \left(x\in A⟼B\right):A⟶C$$
29	27 28	sylibr	$$⊢\phi \to F:A⟶C$$