Theorem dmmptif

Description: Domain of the mapping operation. (Contributed by Glauco Siliprandi, 21-Dec-2024)

	Ref	Expression
Hypotheses	dmmptif.1	$$⊢\underset{\_}{Ⅎ}xA$$
	dmmptif.2	$$⊢B\in \mathrm{V}$$
	dmmptif.3	$$⊢F=\left(x\in A⟼B\right)$$
Assertion	dmmptif	$$⊢\mathrm{dom}F=A$$

Proof

Step	Hyp	Ref	Expression
1		dmmptif.1	$$⊢\underset{\_}{Ⅎ}xA$$
2		dmmptif.2	$$⊢B\in \mathrm{V}$$
3		dmmptif.3	$$⊢F=\left(x\in A⟼B\right)$$
4	1 2 3	fnmptif	$$⊢FFnA$$
5		fndm	$$⊢FFnA\to \mathrm{dom}F=A$$
6	4 5	ax-mp	$$⊢\mathrm{dom}F=A$$