Metamath Proof Explorer


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 A , y B C
Assertion fmpo x A y B C D F : A × B D

Proof

Step Hyp Ref Expression
1 fmpo.1 F = x A , y B C
2 1 fmpox x A y B C D F : x A x × B D
3 iunxpconst x A x × B = A × B
4 3 feq2i F : x A x × B D F : A × B D
5 2 4 bitri x A y B C D F : A × B D