Theorem ovconst2

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

	Ref	Expression
Hypothesis	oprvalconst2.1	$$⊢C\in \mathrm{V}$$
Assertion	ovconst2	$$⊢\left(R\in A\wedge S\in B\right)\to R\left(\left(A\times B\right)\times \left\{C\right\}\right)S=C$$

Proof

Step	Hyp	Ref	Expression
1		oprvalconst2.1	$$⊢C\in \mathrm{V}$$
2		df-ov	$$⊢R\left(\left(A\times B\right)\times \left\{C\right\}\right)S=\left(\left(A\times B\right)\times \left\{C\right\}\right)\left(⟨R,S⟩\right)$$
3		opelxpi	$$⊢\left(R\in A\wedge S\in B\right)\to ⟨R,S⟩\in \left(A\times B\right)$$
4	1	fvconst2	$$⊢⟨R,S⟩\in \left(A\times B\right)\to \left(\left(A\times B\right)\times \left\{C\right\}\right)\left(⟨R,S⟩\right)=C$$
5	3 4	syl	$$⊢\left(R\in A\wedge S\in B\right)\to \left(\left(A\times B\right)\times \left\{C\right\}\right)\left(⟨R,S⟩\right)=C$$
6	2 5	eqtrid	$$⊢\left(R\in A\wedge S\in B\right)\to R\left(\left(A\times B\right)\times \left\{C\right\}\right)S=C$$