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

Metamath Proof Explorer

Theorem ovres

Description: The value of a restricted operation. (Contributed by FL, 10-Nov-2006)

		Ref	Expression
	Assertion	ovres	$⊢ (A \in C \land B \in D) \to A ({F ↾}_{(C \times D)}) B = A F B$

Step	Hyp	Ref	Expression
1		opelxpi	$⊢ (A \in C \land B \in D) \to ⟨A, B⟩ \in (C \times D)$
2	1	fvresd	$⊢ (A \in C \land B \in D) \to ({F ↾}_{(C \times D)}) (⟨A, B⟩) = F (⟨A, B⟩)$
3		df-ov	$⊢ A ({F ↾}_{(C \times D)}) B = ({F ↾}_{(C \times D)}) (⟨A, B⟩)$
4		df-ov	$⊢ A F B = F (⟨A, B⟩)$
5	2 3 4	3eqtr4g	$⊢ (A \in C \land B \in D) \to A ({F ↾}_{(C \times D)}) B = A F B$