Metamath Proof Explorer

Theorem ovmpox

Description: The value of an operation class abstraction. Variant of ovmpoga which does not require D and x to be distinct. (Contributed by Jeff Madsen, 10-Jun-2010) (Revised by Mario Carneiro, 20-Dec-2013)

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

Proof

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