Theorem fnrnov

Description: The range of an operation expressed as a collection of the operation's values. (Contributed by NM, 29-Oct-2006)

	Ref	Expression
Assertion	fnrnov	$$⊢FFn\left(A\times B\right)\to \mathrm{ran}F=\left\{z|\exists x\in A\exists y\in Bz=xFy\right\}$$

Proof

Step	Hyp	Ref	Expression
1		fnrnfv	$$⊢FFn\left(A\times B\right)\to \mathrm{ran}F=\left\{z|\exists w\in \left(A\times B\right)z=F\left(w\right)\right\}$$
2		fveq2	$$⊢w=⟨x,y⟩\to F\left(w\right)=F\left(⟨x,y⟩\right)$$
3		df-ov	$$⊢xFy=F\left(⟨x,y⟩\right)$$
4	2 3	eqtr4di	$$⊢w=⟨x,y⟩\to F\left(w\right)=xFy$$
5	4	eqeq2d	$$⊢w=⟨x,y⟩\to \left(z=F\left(w\right)\leftrightarrow z=xFy\right)$$
6	5	rexxp	$$⊢\exists w\in \left(A\times B\right)z=F\left(w\right)\leftrightarrow \exists x\in A\exists y\in Bz=xFy$$
7	6	abbii	$$⊢\left\{z|\exists w\in \left(A\times B\right)z=F\left(w\right)\right\}=\left\{z|\exists x\in A\exists y\in Bz=xFy\right\}$$
8	1 7	eqtrdi	$$⊢FFn\left(A\times B\right)\to \mathrm{ran}F=\left\{z|\exists x\in A\exists y\in Bz=xFy\right\}$$