oprssov

Description: The value of a member of the domain of a subclass of an operation. (Contributed by NM, 23-Aug-2007)

		Ref	Expression
	Assertion	oprssov	$⊢ ((Fun F \land G Fn (C \times D) \land G \subseteq F) \land (A \in C \land B \in D)) \to A F B = A G B$

Step	Hyp	Ref	Expression
1		ovres	$⊢ (A \in C \land B \in D) \to A ({F ↾}_{(C \times D)}) B = A F B$
2	1	adantl	$⊢ ((Fun F \land G Fn (C \times D) \land G \subseteq F) \land (A \in C \land B \in D)) \to A ({F ↾}_{(C \times D)}) B = A F B$
3		fndm	$⊢ G Fn (C \times D) \to dom G = C \times D$
4	3	reseq2d	$⊢ G Fn (C \times D) \to {F ↾}_{dom G} = {F ↾}_{(C \times D)}$
5	4	3ad2ant2	$⊢ (Fun F \land G Fn (C \times D) \land G \subseteq F) \to {F ↾}_{dom G} = {F ↾}_{(C \times D)}$
6		funssres	$⊢ (Fun F \land G \subseteq F) \to {F ↾}_{dom G} = G$
7	6	3adant2	$⊢ (Fun F \land G Fn (C \times D) \land G \subseteq F) \to {F ↾}_{dom G} = G$
8	5 7	eqtr3d	$⊢ (Fun F \land G Fn (C \times D) \land G \subseteq F) \to {F ↾}_{(C \times D)} = G$
9	8	oveqd	$⊢ (Fun F \land G Fn (C \times D) \land G \subseteq F) \to A ({F ↾}_{(C \times D)}) B = A G B$
10	9	adantr	$⊢ ((Fun F \land G Fn (C \times D) \land G \subseteq F) \land (A \in C \land B \in D)) \to A ({F ↾}_{(C \times D)}) B = A G B$
11	2 10	eqtr3d	$⊢ ((Fun F \land G Fn (C \times D) \land G \subseteq F) \land (A \in C \land B \in D)) \to A F B = A G B$

Metamath Proof Explorer