Theorem fmptdff

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

	Ref	Expression
Hypotheses	fmptdff.1	$$⊢Ⅎx\phi$$
	fmptdff.2	$$⊢\underset{\_}{Ⅎ}xA$$
	fmptdff.3	$$⊢\underset{\_}{Ⅎ}xC$$
	fmptdff.4	$$⊢\left(\phi \wedge x\in A\right)\to B\in C$$
	fmptdff.5	$$⊢F=\left(x\in A⟼B\right)$$
Assertion	fmptdff	$$⊢\phi \to F:A⟶C$$

Proof

Step	Hyp	Ref	Expression
1		fmptdff.1	$$⊢Ⅎx\phi$$
2		fmptdff.2	$$⊢\underset{\_}{Ⅎ}xA$$
3		fmptdff.3	$$⊢\underset{\_}{Ⅎ}xC$$
4		fmptdff.4	$$⊢\left(\phi \wedge x\in A\right)\to B\in C$$
5		fmptdff.5	$$⊢F=\left(x\in A⟼B\right)$$
6	1 4	ralrimia	$$⊢\phi \to \forall x\in AB\in C$$
7	2 3 5	fmptff	$$⊢\forall x\in AB\in C\leftrightarrow F:A⟶C$$
8	6 7	sylib	$$⊢\phi \to F:A⟶C$$