Theorem dmmpt

Description: The domain of the mapping operation in general. (Contributed by NM, 16-May-1995) (Revised by Mario Carneiro, 22-Mar-2015)

	Ref	Expression
Hypothesis	dmmpt.1	|- F = ( x e. A |-> B )
Assertion	dmmpt	|- dom F = { x e. A | B e. _V }

Proof

Step	Hyp	Ref	Expression
1		dmmpt.1	|- F = ( x e. A |-> B )
2		dfdm4	|- dom F = ran `' F
3		dfrn4	|- ran `' F = ( `' F " _V )
4	1	mptpreima	|- ( `' F " _V ) = { x e. A | B e. _V }
5	2 3 4	3eqtri	|- dom F = { x e. A | B e. _V }