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 = ( x e. A , y e. B |-> C )
Assertion	fmpo	|- ( A. x e. A A. y e. B C e. D <-> F : ( A X. B ) --> D )

Proof

Step	Hyp	Ref	Expression
1		fmpo.1	|- F = ( x e. A , y e. B |-> C )
2	1	fmpox	|- ( A. x e. A A. y e. B C e. D <-> F : U_ x e. A ( { x } X. B ) --> D )
3		iunxpconst	|- U_ x e. A ( { x } X. B ) = ( A X. B )
4	3	feq2i	|- ( F : U_ x e. A ( { x } X. B ) --> D <-> F : ( A X. B ) --> D )
5	2 4	bitri	|- ( A. x e. A A. y e. B C e. D <-> F : ( A X. B ) --> D )