Metamath Proof Explorer


Theorem dmmpo

Description: 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 dmmpo dom F = A × B

Proof

Step Hyp Ref Expression
1 fmpo.1 F = x A , y B C
2 fnmpoi.2 C V
3 1 2 fnmpoi F Fn A × B
4 3 fndmi dom F = A × B