Theorem ovconst2

Description: The value of a constant operation. (Contributed by NM, 5-Nov-2006)

	Ref	Expression
Hypothesis	oprvalconst2.1	⊢ 𝐶 ∈ V
Assertion	ovconst2	⊢ ( ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐵 ) → ( 𝑅 ( ( 𝐴 × 𝐵 ) × { 𝐶 } ) 𝑆 ) = 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		oprvalconst2.1	⊢ 𝐶 ∈ V
2		df-ov	⊢ ( 𝑅 ( ( 𝐴 × 𝐵 ) × { 𝐶 } ) 𝑆 ) = ( ( ( 𝐴 × 𝐵 ) × { 𝐶 } ) ‘ ⟨ 𝑅 , 𝑆 ⟩ )
3		opelxpi	⊢ ( ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐵 ) → ⟨ 𝑅 , 𝑆 ⟩ ∈ ( 𝐴 × 𝐵 ) )
4	1	fvconst2	⊢ ( ⟨ 𝑅 , 𝑆 ⟩ ∈ ( 𝐴 × 𝐵 ) → ( ( ( 𝐴 × 𝐵 ) × { 𝐶 } ) ‘ ⟨ 𝑅 , 𝑆 ⟩ ) = 𝐶 )
5	3 4	syl	⊢ ( ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐵 ) → ( ( ( 𝐴 × 𝐵 ) × { 𝐶 } ) ‘ ⟨ 𝑅 , 𝑆 ⟩ ) = 𝐶 )
6	2 5	eqtrid	⊢ ( ( 𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐵 ) → ( 𝑅 ( ( 𝐴 × 𝐵 ) × { 𝐶 } ) 𝑆 ) = 𝐶 )