This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ovigg

Description: The value of an operation class abstraction. Compared with ovig , the condition ( x e. R /\ y e. S ) is removed. (Contributed by FL, 24-Mar-2007) (Revised by Mario Carneiro, 19-Dec-2013)

		Ref	Expression
	Hypotheses	ovigg.1	$⊢ (x = A \land y = B \land z = C) \to (φ \leftrightarrow ψ)$
		ovigg.4	$⊢ \exists^{*} z φ$
		ovigg.5	$⊢ F = \{⟨⟨x, y⟩, z⟩ \| φ\}$
	Assertion	ovigg	$⊢ (A \in V \land B \in W \land C \in X) \to (ψ \to A F B = C)$

Proof

Step	Hyp	Ref	Expression
1		ovigg.1	$⊢ (x = A \land y = B \land z = C) \to (φ \leftrightarrow ψ)$
2		ovigg.4	$⊢ \exists^{*} z φ$
3		ovigg.5	$⊢ F = \{⟨⟨x, y⟩, z⟩ \| φ\}$
4	1	eloprabga	$⊢ (A \in V \land B \in W \land C \in X) \to (⟨⟨A, B⟩, C⟩ \in \{⟨⟨x, y⟩, z⟩ \| φ\} \leftrightarrow ψ)$
5		df-ov	$⊢ A F B = F (⟨A, B⟩)$
6	3	fveq1i	$⊢ F (⟨A, B⟩) = \{⟨⟨x, y⟩, z⟩ \| φ\} (⟨A, B⟩)$
7	5 6	eqtri	$⊢ A F B = \{⟨⟨x, y⟩, z⟩ \| φ\} (⟨A, B⟩)$
8	2	funoprab	$⊢ Fun \{⟨⟨x, y⟩, z⟩ \| φ\}$
9		funopfv	$⊢ Fun \{⟨⟨x, y⟩, z⟩ \| φ\} \to (⟨⟨A, B⟩, C⟩ \in \{⟨⟨x, y⟩, z⟩ \| φ\} \to \{⟨⟨x, y⟩, z⟩ \| φ\} (⟨A, B⟩) = C)$
10	8 9	ax-mp	$⊢ ⟨⟨A, B⟩, C⟩ \in \{⟨⟨x, y⟩, z⟩ \| φ\} \to \{⟨⟨x, y⟩, z⟩ \| φ\} (⟨A, B⟩) = C$
11	7 10	eqtrid	$⊢ ⟨⟨A, B⟩, C⟩ \in \{⟨⟨x, y⟩, z⟩ \| φ\} \to A F B = C$
12	4 11	biimtrrdi	$⊢ (A \in V \land B \in W \land C \in X) \to (ψ \to A F B = C)$