Theorem ofcfeqd2

Description: Equality theorem for function/constant operation value. (Contributed by Thierry Arnoux, 31-Jan-2017)

	Ref	Expression
Hypotheses	ofcfeqd2.1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 )
	ofcfeqd2.2	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑦 𝑅 𝐶 ) = ( 𝑦 𝑃 𝐶 ) )
	ofcfeqd2.3	⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
	ofcfeqd2.4	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	ofcfeqd2.5	⊢ ( 𝜑 → 𝐶 ∈ 𝑊 )
Assertion	ofcfeqd2	⊢ ( 𝜑 → ( 𝐹 ∘f/c 𝑅 𝐶 ) = ( 𝐹 ∘f/c 𝑃 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		ofcfeqd2.1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 )
2		ofcfeqd2.2	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑦 𝑅 𝐶 ) = ( 𝑦 𝑃 𝐶 ) )
3		ofcfeqd2.3	⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
4		ofcfeqd2.4	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
5		ofcfeqd2.5	⊢ ( 𝜑 → 𝐶 ∈ 𝑊 )
6		oveq1	⊢ ( 𝑦 = ( 𝐹 ‘ 𝑥 ) → ( 𝑦 𝑅 𝐶 ) = ( ( 𝐹 ‘ 𝑥 ) 𝑅 𝐶 ) )
7		oveq1	⊢ ( 𝑦 = ( 𝐹 ‘ 𝑥 ) → ( 𝑦 𝑃 𝐶 ) = ( ( 𝐹 ‘ 𝑥 ) 𝑃 𝐶 ) )
8	6 7	eqeq12d	⊢ ( 𝑦 = ( 𝐹 ‘ 𝑥 ) → ( ( 𝑦 𝑅 𝐶 ) = ( 𝑦 𝑃 𝐶 ) ↔ ( ( 𝐹 ‘ 𝑥 ) 𝑅 𝐶 ) = ( ( 𝐹 ‘ 𝑥 ) 𝑃 𝐶 ) ) )
9	2	ralrimiva	⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐵 ( 𝑦 𝑅 𝐶 ) = ( 𝑦 𝑃 𝐶 ) )
10	9	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∀ 𝑦 ∈ 𝐵 ( 𝑦 𝑅 𝐶 ) = ( 𝑦 𝑃 𝐶 ) )
11	8 10 1	rspcdva	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑥 ) 𝑅 𝐶 ) = ( ( 𝐹 ‘ 𝑥 ) 𝑃 𝐶 ) )
12	11	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑅 𝐶 ) ) = ( 𝑥 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑃 𝐶 ) ) )
13		eqidd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
14	3 4 5 13	ofcfval	⊢ ( 𝜑 → ( 𝐹 ∘f/c 𝑅 𝐶 ) = ( 𝑥 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑅 𝐶 ) ) )
15	3 4 5 13	ofcfval	⊢ ( 𝜑 → ( 𝐹 ∘f/c 𝑃 𝐶 ) = ( 𝑥 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑥 ) 𝑃 𝐶 ) ) )
16	12 14 15	3eqtr4d	⊢ ( 𝜑 → ( 𝐹 ∘f/c 𝑅 𝐶 ) = ( 𝐹 ∘f/c 𝑃 𝐶 ) )