Theorem fmptdf

Description: A version of fmptd using bound-variable hypothesis instead of a distinct variable condition for ph . (Contributed by Glauco Siliprandi, 29-Jun-2017)

	Ref	Expression
Hypotheses	fmptdf.1	$$⊢Ⅎx\phi$$
	fmptdf.2	$$⊢\left(\phi \wedge x\in A\right)\to B\in C$$
	fmptdf.3	$$⊢F=\left(x\in A⟼B\right)$$
Assertion	fmptdf	$$⊢\phi \to F:A⟶C$$

Proof

Step	Hyp	Ref	Expression
1		fmptdf.1	$$⊢Ⅎx\phi$$
2		fmptdf.2	$$⊢\left(\phi \wedge x\in A\right)\to B\in C$$
3		fmptdf.3	$$⊢F=\left(x\in A⟼B\right)$$
4	2	ex	$$⊢\phi \to \left(x\in A\to B\in C\right)$$
5	1 4	ralrimi	$$⊢\phi \to \forall x\in AB\in C$$
6	3	fmpt	$$⊢\forall x\in AB\in C\leftrightarrow F:A⟶C$$
7	5 6	sylib	$$⊢\phi \to F:A⟶C$$