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 e. A , y e. B |-> C )
fnmpoi.2
|- C e. _V
Assertion dmmpo
|- dom F = ( A X. B )

Proof

Step Hyp Ref Expression
1 fmpo.1
 |-  F = ( x e. A , y e. B |-> C )
2 fnmpoi.2
 |-  C e. _V
3 1 2 fnmpoi
 |-  F Fn ( A X. B )
4 3 fndmi
 |-  dom F = ( A X. B )