Theorem offveqb

Description: Equivalent expressions for equality with a function operation. (Contributed by NM, 9-Oct-2014) (Proof shortened by Mario Carneiro, 5-Dec-2016)

	Ref	Expression
Hypotheses	offveq.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	offveq.2	⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
	offveq.3	⊢ ( 𝜑 → 𝐺 Fn 𝐴 )
	offveq.4	⊢ ( 𝜑 → 𝐻 Fn 𝐴 )
	offveq.5	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = 𝐵 )
	offveq.6	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑥 ) = 𝐶 )
Assertion	offveqb	⊢ ( 𝜑 → ( 𝐻 = ( 𝐹 ∘f 𝑅 𝐺 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐻 ‘ 𝑥 ) = ( 𝐵 𝑅 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		offveq.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		offveq.2	⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
3		offveq.3	⊢ ( 𝜑 → 𝐺 Fn 𝐴 )
4		offveq.4	⊢ ( 𝜑 → 𝐻 Fn 𝐴 )
5		offveq.5	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = 𝐵 )
6		offveq.6	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑥 ) = 𝐶 )
7		dffn5	⊢ ( 𝐻 Fn 𝐴 ↔ 𝐻 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐻 ‘ 𝑥 ) ) )
8	4 7	sylib	⊢ ( 𝜑 → 𝐻 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐻 ‘ 𝑥 ) ) )
9		inidm	⊢ ( 𝐴 ∩ 𝐴 ) = 𝐴
10	2 3 1 1 9 5 6	offval	⊢ ( 𝜑 → ( 𝐹 ∘f 𝑅 𝐺 ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 𝑅 𝐶 ) ) )
11	8 10	eqeq12d	⊢ ( 𝜑 → ( 𝐻 = ( 𝐹 ∘f 𝑅 𝐺 ) ↔ ( 𝑥 ∈ 𝐴 ↦ ( 𝐻 ‘ 𝑥 ) ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 𝑅 𝐶 ) ) ) )
12		fvexd	⊢ ( 𝜑 → ( 𝐻 ‘ 𝑥 ) ∈ V )
13	12	ralrimivw	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ( 𝐻 ‘ 𝑥 ) ∈ V )
14		mpteqb	⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝐻 ‘ 𝑥 ) ∈ V → ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐻 ‘ 𝑥 ) ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 𝑅 𝐶 ) ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐻 ‘ 𝑥 ) = ( 𝐵 𝑅 𝐶 ) ) )
15	13 14	syl	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐻 ‘ 𝑥 ) ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 𝑅 𝐶 ) ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐻 ‘ 𝑥 ) = ( 𝐵 𝑅 𝐶 ) ) )
16	11 15	bitrd	⊢ ( 𝜑 → ( 𝐻 = ( 𝐹 ∘f 𝑅 𝐺 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐻 ‘ 𝑥 ) = ( 𝐵 𝑅 𝐶 ) ) )