Metamath Proof Explorer

Theorem fnmpoi

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

Ref Expression
Hypotheses fmpo.1 F = x A , y B C
fnmpoi.2 C V
Assertion fnmpoi F Fn A × B


Step Hyp Ref Expression
1 fmpo.1 F = x A , y B C
2 fnmpoi.2 C V
3 2 rgen2w x A y B C V
4 1 fnmpo x A y B C V F Fn A × B
5 3 4 ax-mp F Fn A × B