Theorem ovelimab

Description: Operation value in an image. (Contributed by Mario Carneiro, 23-Dec-2013) (Revised by Mario Carneiro, 29-Jan-2014)

	Ref	Expression
Assertion	ovelimab	$$⊢\left(FFnA\wedge B\times C\subseteq A\right)\to \left(D\in F\left[B\times C\right]\leftrightarrow \exists x\in B\exists y\in CD=xFy\right)$$

Proof

Step	Hyp	Ref	Expression
1		fvelimab	$$⊢\left(FFnA\wedge B\times C\subseteq A\right)\to \left(D\in F\left[B\times C\right]\leftrightarrow \exists z\in \left(B\times C\right)F\left(z\right)=D\right)$$
2		fveq2	$$⊢z=⟨x,y⟩\to F\left(z\right)=F\left(⟨x,y⟩\right)$$
3		df-ov	$$⊢xFy=F\left(⟨x,y⟩\right)$$
4	2 3	eqtr4di	$$⊢z=⟨x,y⟩\to F\left(z\right)=xFy$$
5	4	eqeq1d	$$⊢z=⟨x,y⟩\to \left(F\left(z\right)=D\leftrightarrow xFy=D\right)$$
6		eqcom	$$⊢xFy=D\leftrightarrow D=xFy$$
7	5 6	bitrdi	$$⊢z=⟨x,y⟩\to \left(F\left(z\right)=D\leftrightarrow D=xFy\right)$$
8	7	rexxp	$$⊢\exists z\in \left(B\times C\right)F\left(z\right)=D\leftrightarrow \exists x\in B\exists y\in CD=xFy$$
9	1 8	bitrdi	$$⊢\left(FFnA\wedge B\times C\subseteq A\right)\to \left(D\in F\left[B\times C\right]\leftrightarrow \exists x\in B\exists y\in CD=xFy\right)$$