Metamath Proof Explorer

Theorem dmmpti

Description: Domain of the mapping operation. (Contributed by NM, 6-Sep-2005) (Revised by Mario Carneiro, 31-Aug-2015)

Ref Expression
Hypotheses fnmpti.1 B V
fnmpti.2 F = x A B
Assertion dmmpti dom F = A


Step Hyp Ref Expression
1 fnmpti.1 B V
2 fnmpti.2 F = x A B
3 1 2 fnmpti F Fn A
4 3 fndmi dom F = A