Theorem fmpt3d

Description: Domain and codomain of the mapping operation; deduction form. (Contributed by Thierry Arnoux, 4-Jun-2017)

	Ref	Expression
Hypotheses	fmpt3d.1	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
	fmpt3d.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝐶 )
Assertion	fmpt3d	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		fmpt3d.1	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
2		fmpt3d.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝐶 )
3	2	fmpttd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ 𝐶 )
4	1	feq1d	⊢ ( 𝜑 → ( 𝐹 : 𝐴 ⟶ 𝐶 ↔ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ 𝐶 ) )
5	3 4	mpbird	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐶 )