Theorem fmpo

Description: Functionality, domain and range of a class given by the maps-to notation. (Contributed by FL, 17-May-2010)

	Ref	Expression
Hypothesis	fmpo.1	$$⊢F=\left(x\in A,y\in B⟼C\right)$$
Assertion	fmpo	$$⊢\forall x\in A\forall y\in BC\in D\leftrightarrow F:A\times B⟶D$$

Proof

Step	Hyp	Ref	Expression
1		fmpo.1	$$⊢F=\left(x\in A,y\in B⟼C\right)$$
2	1	fmpox	$$⊢\forall x\in A\forall y\in BC\in D\leftrightarrow F:\bigcup _{x\in A}\left(\left\{x\right\}\times B\right)⟶D$$
3		iunxpconst	$$⊢\bigcup _{x\in A}\left(\left\{x\right\}\times B\right)=A\times B$$
4	3	feq2i	$$⊢F:\bigcup _{x\in A}\left(\left\{x\right\}\times B\right)⟶D\leftrightarrow F:A\times B⟶D$$
5	2 4	bitri	$$⊢\forall x\in A\forall y\in BC\in D\leftrightarrow F:A\times B⟶D$$