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 e. _V
fnmpti.2 
|- F = ( x e. A |-> B )
Assertion dmmpti 
|- dom F = A

Proof

Step Hyp Ref Expression
1 fnmpti.1 
 |-  B e. _V
2 fnmpti.2 
 |-  F = ( x e. A |-> B )
3 1 2 fnmpti 
 |-  F Fn A
4 3 fndmi 
 |-  dom F = A