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=\left(x\in A⟼B\right)$$
Assertion	dmmpt	$$⊢\mathrm{dom}F=\left\{x\in A|B\in \mathrm{V}\right\}$$

Proof

Step	Hyp	Ref	Expression
1		dmmpt.1	$$⊢F=\left(x\in A⟼B\right)$$
2		dfdm4	$$⊢\mathrm{dom}F=\mathrm{ran}{F}^{-1}$$
3		dfrn4	$$⊢\mathrm{ran}{F}^{-1}=F^{-1}\left[\mathrm{V}\right]$$
4	1	mptpreima	$$⊢F^{-1}\left[\mathrm{V}\right]=\left\{x\in A|B\in \mathrm{V}\right\}$$
5	2 3 4	3eqtri	$$⊢\mathrm{dom}F=\left\{x\in A|B\in \mathrm{V}\right\}$$