ovmpoga

Description: Value of an operation given by a maps-to rule. (Contributed by Mario Carneiro, 19-Dec-2013)

	Ref	Expression
Hypotheses	ovmpoga.1	$⊢ (x = A \land y = B) \to R = S$
	ovmpoga.2	$⊢ F = (x \in C, y \in D ⟼ R)$
Assertion	ovmpoga	$⊢ (A \in C \land B \in D \land S \in H) \to A F B = S$

Step	Hyp	Ref	Expression
1		ovmpoga.1	$⊢ (x = A \land y = B) \to R = S$
2		ovmpoga.2	$⊢ F = (x \in C, y \in D ⟼ R)$
3		elex	$⊢ S \in H \to S \in V$
4	2	a1i	$⊢ (A \in C \land B \in D \land S \in V) \to F = (x \in C, y \in D ⟼ R)$
5	1	adantl	$⊢ ((A \in C \land B \in D \land S \in V) \land (x = A \land y = B)) \to R = S$
6		simp1	$⊢ (A \in C \land B \in D \land S \in V) \to A \in C$
7		simp2	$⊢ (A \in C \land B \in D \land S \in V) \to B \in D$
8		simp3	$⊢ (A \in C \land B \in D \land S \in V) \to S \in V$
9	4 5 6 7 8	ovmpod	$⊢ (A \in C \land B \in D \land S \in V) \to A F B = S$
10	3 9	syl3an3	$⊢ (A \in C \land B \in D \land S \in H) \to A F B = S$

Metamath Proof Explorer