This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ovconst2

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

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

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