Metamath Proof Explorer

Theorem ovmpox2

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	ovmpox2.1	$⊢ (x = A \land y = B) \to R = S$
		ovmpox2.2	$⊢ y = B \to C = L$
		ovmpox2.3	$⊢ F = (x \in C, y \in D ⟼ R)$
	Assertion	ovmpox2	$⊢ (A \in L \land B \in D \land S \in H) \to A F B = S$

Proof

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