Metamath Proof Explorer

Theorem ovig

Description: The value of an operation class abstraction (weak version). (Contributed by NM, 14-Sep-1999) Remove unnecessary distinct variable conditions. (Revised by David Abernethy, 19-Jun-2012) (Revised by Mario Carneiro, 19-Dec-2013)

		Ref	Expression
	Hypotheses	ovig.1	$⊢ (x = A \land y = B \land z = C) \to (φ \leftrightarrow ψ)$
		ovig.2	$⊢ (x \in R \land y \in S) \to \exists^{*} z φ$
		ovig.3	$⊢ F = \{⟨⟨x, y⟩, z⟩ \| ((x \in R \land y \in S) \land φ)\}$
	Assertion	ovig	$⊢ (A \in R \land B \in S \land C \in D) \to (ψ \to A F B = C)$

Proof

Step	Hyp	Ref	Expression
1		ovig.1	$⊢ (x = A \land y = B \land z = C) \to (φ \leftrightarrow ψ)$
2		ovig.2	$⊢ (x \in R \land y \in S) \to \exists^{*} z φ$
3		ovig.3	$⊢ F = \{⟨⟨x, y⟩, z⟩ \| ((x \in R \land y \in S) \land φ)\}$
4		3simpa	$⊢ (A \in R \land B \in S \land C \in D) \to (A \in R \land B \in S)$
5		eleq1	$⊢ x = A \to (x \in R \leftrightarrow A \in R)$
6		eleq1	$⊢ y = B \to (y \in S \leftrightarrow B \in S)$
7	5 6	bi2anan9	$⊢ (x = A \land y = B) \to ((x \in R \land y \in S) \leftrightarrow (A \in R \land B \in S))$
8	7	3adant3	$⊢ (x = A \land y = B \land z = C) \to ((x \in R \land y \in S) \leftrightarrow (A \in R \land B \in S))$
9	8 1	anbi12d	$⊢ (x = A \land y = B \land z = C) \to (((x \in R \land y \in S) \land φ) \leftrightarrow ((A \in R \land B \in S) \land ψ))$
10		moanimv	$⊢ \exists^{} z ((x \in R \land y \in S) \land φ) \leftrightarrow ((x \in R \land y \in S) \to \exists^{} z φ)$
11	2 10	mpbir	$⊢ \exists^{*} z ((x \in R \land y \in S) \land φ)$
12	9 11 3	ovigg	$⊢ (A \in R \land B \in S \land C \in D) \to (((A \in R \land B \in S) \land ψ) \to A F B = C)$
13	4 12	mpand	$⊢ (A \in R \land B \in S \land C \in D) \to (ψ \to A F B = C)$