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\phi$$
	ovidig.2	$$⊢F=\left\{⟨⟨x,y⟩,z⟩|\phi \right\}$$
Assertion	ovidig	$$⊢\phi \to xFy=z$$

Proof

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