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

Metamath Proof Explorer

Theorem ovidig

Description: The value of an operation class abstraction. Compare ovidi . The condition ( x e. R /\ y e. S ) is been removed. (Contributed by Mario Carneiro, 29-Dec-2014)

		Ref	Expression
	Hypotheses	ovidig.1	$⊢ \exists^{*} z φ$
		ovidig.2	$⊢ F = \{⟨⟨x, y⟩, z⟩ \| φ\}$
	Assertion	ovidig	$⊢ φ \to x F y = z$

Proof

Step	Hyp	Ref	Expression
1		ovidig.1	$⊢ \exists^{*} z φ$
2		ovidig.2	$⊢ F = \{⟨⟨x, y⟩, z⟩ \| φ\}$
3		df-ov	$⊢ x F y = F (⟨x, y⟩)$
4	1	funoprab	$⊢ Fun \{⟨⟨x, y⟩, z⟩ \| φ\}$
5	2	funeqi	$⊢ Fun F \leftrightarrow Fun \{⟨⟨x, y⟩, z⟩ \| φ\}$
6	4 5	mpbir	$⊢ Fun F$
7		oprabidw	$⊢ ⟨⟨x, y⟩, z⟩ \in \{⟨⟨x, y⟩, z⟩ \| φ\} \leftrightarrow φ$
8	7	biimpri	$⊢ φ \to ⟨⟨x, y⟩, z⟩ \in \{⟨⟨x, y⟩, z⟩ \| φ\}$
9	8 2	eleqtrrdi	$⊢ φ \to ⟨⟨x, y⟩, z⟩ \in F$
10		funopfv	$⊢ Fun F \to (⟨⟨x, y⟩, z⟩ \in F \to F (⟨x, y⟩) = z)$
11	6 9 10	mpsyl	$⊢ φ \to F (⟨x, y⟩) = z$
12	3 11	eqtrid	$⊢ φ \to x F y = z$