Theorem cofmpt

Description: Express composition of a maps-to function with another function in a maps-to notation. (Contributed by Thierry Arnoux, 29-Jun-2017)

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

Proof

Step	Hyp	Ref	Expression
1		cofmpt.1	⊢ ( 𝜑 → 𝐹 : 𝐶 ⟶ 𝐷 )
2		cofmpt.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝐶 )
3		eqidd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
4	1	feqmptd	⊢ ( 𝜑 → 𝐹 = ( 𝑦 ∈ 𝐶 ↦ ( 𝐹 ‘ 𝑦 ) ) )
5		fveq2	⊢ ( 𝑦 = 𝐵 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝐵 ) )
6	2 3 4 5	fmptco	⊢ ( 𝜑 → ( 𝐹 ∘ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝐵 ) ) )