Theorem ovidi

Description: The value of an operation class abstraction (weak version). (Contributed by Mario Carneiro, 29-Dec-2014)

	Ref	Expression
Hypotheses	ovidi.2	$$⊢\left(x\in R\wedge y\in S\right)\to {\exists }^{*}z\phi$$
	ovidi.3	$$⊢F=\left\{⟨⟨x,y⟩,z⟩|\left(\left(x\in R\wedge y\in S\right)\wedge \phi \right)\right\}$$
Assertion	ovidi	$$⊢\left(x\in R\wedge y\in S\right)\to \left(\phi \to xFy=z\right)$$

Proof

Step	Hyp	Ref	Expression
1		ovidi.2	$$⊢\left(x\in R\wedge y\in S\right)\to {\exists }^{*}z\phi$$
2		ovidi.3	$$⊢F=\left\{⟨⟨x,y⟩,z⟩|\left(\left(x\in R\wedge y\in S\right)\wedge \phi \right)\right\}$$
3		moanimv	$$⊢{\exists }^{*}z\left(\left(x\in R\wedge y\in S\right)\wedge \phi \right)\leftrightarrow \left(\left(x\in R\wedge y\in S\right)\to {\exists }^{*}z\phi \right)$$
4	1 3	mpbir	$$⊢{\exists }^{*}z\left(\left(x\in R\wedge y\in S\right)\wedge \phi \right)$$
5	4 2	ovidig	$$⊢\left(\left(x\in R\wedge y\in S\right)\wedge \phi \right)\to xFy=z$$
6	5	ex	$$⊢\left(x\in R\wedge y\in S\right)\to \left(\phi \to xFy=z\right)$$