Theorem funimassov

Description: Membership relation for the values of a function whose image is a subclass. (Contributed by Mario Carneiro, 23-Dec-2013)

	Ref	Expression
Assertion	funimassov	$$⊢\left(\mathrm{Fun}F\wedge A\times B\subseteq \mathrm{dom}F\right)\to \left(F\left[A\times B\right]\subseteq C\leftrightarrow \forall x\in A\forall y\in BxFy\in C\right)$$

Proof

Step	Hyp	Ref	Expression
1		funimass4	$$⊢\left(\mathrm{Fun}F\wedge A\times B\subseteq \mathrm{dom}F\right)\to \left(F\left[A\times B\right]\subseteq C\leftrightarrow \forall z\in \left(A\times B\right)F\left(z\right)\in C\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	eleq1d	$$⊢z=⟨x,y⟩\to \left(F\left(z\right)\in C\leftrightarrow xFy\in C\right)$$
6	5	ralxp	$$⊢\forall z\in \left(A\times B\right)F\left(z\right)\in C\leftrightarrow \forall x\in A\forall y\in BxFy\in C$$
7	1 6	bitrdi	$$⊢\left(\mathrm{Fun}F\wedge A\times B\subseteq \mathrm{dom}F\right)\to \left(F\left[A\times B\right]\subseteq C\leftrightarrow \forall x\in A\forall y\in BxFy\in C\right)$$