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	⊢ Ⅎ 𝑥 𝜑
	fmptdff.2	⊢ Ⅎ 𝑥 𝐴
	fmptdff.3	⊢ Ⅎ 𝑥 𝐶
	fmptdff.4	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝐶 )
	fmptdff.5	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
Assertion	fmptdff	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		fmptdff.1	⊢ Ⅎ 𝑥 𝜑
2		fmptdff.2	⊢ Ⅎ 𝑥 𝐴
3		fmptdff.3	⊢ Ⅎ 𝑥 𝐶
4		fmptdff.4	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝐶 )
5		fmptdff.5	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
6	1 4	ralrimia	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 )
7	2 3 5	fmptff	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ↔ 𝐹 : 𝐴 ⟶ 𝐶 )
8	6 7	sylib	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐶 )