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	|- F/ x ph
	fmptdff.2	|- F/_ x A
	fmptdff.3	|- F/_ x C
	fmptdff.4	|- ( ( ph /\ x e. A ) -> B e. C )
	fmptdff.5	|- F = ( x e. A |-> B )
Assertion	fmptdff	|- ( ph -> F : A --> C )

Proof

Step	Hyp	Ref	Expression
1		fmptdff.1	|- F/ x ph
2		fmptdff.2	|- F/_ x A
3		fmptdff.3	|- F/_ x C
4		fmptdff.4	|- ( ( ph /\ x e. A ) -> B e. C )
5		fmptdff.5	|- F = ( x e. A |-> B )
6	1 4	ralrimia	|- ( ph -> A. x e. A B e. C )
7	2 3 5	fmptff	|- ( A. x e. A B e. C <-> F : A --> C )
8	6 7	sylib	|- ( ph -> F : A --> C )