Theorem ofcfval2

Description: The function operation expressed as a mapping. (Contributed by Thierry Arnoux, 31-Jan-2017)

	Ref	Expression
Hypotheses	ofcfval2.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	ofcfval2.2	⊢ ( 𝜑 → 𝐶 ∈ 𝑊 )
	ofcfval2.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑋 )
	ofcfval2.4	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
Assertion	ofcfval2	⊢ ( 𝜑 → ( 𝐹 ∘f/c 𝑅 𝐶 ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 𝑅 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ofcfval2.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		ofcfval2.2	⊢ ( 𝜑 → 𝐶 ∈ 𝑊 )
3		ofcfval2.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑋 )
4		ofcfval2.4	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
5	3	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑋 )
6		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
7	6	fnmpt	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑋 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) Fn 𝐴 )
8	5 7	syl	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) Fn 𝐴 )
9	4	fneq1d	⊢ ( 𝜑 → ( 𝐹 Fn 𝐴 ↔ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) Fn 𝐴 ) )
10	8 9	mpbird	⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
11	4 3	fvmpt2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = 𝐵 )
12	10 1 2 11	ofcfval	⊢ ( 𝜑 → ( 𝐹 ∘f/c 𝑅 𝐶 ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 𝑅 𝐶 ) ) )