Theorem dmmptdf

Description: The domain of the mapping operation, deduction form. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	dmmptdf.x	$$⊢Ⅎx\phi$$
	dmmptdf.a	$$⊢A=\left(x\in B⟼C\right)$$
	dmmptdf.c	$$⊢\left(\phi \wedge x\in B\right)\to C\in V$$
Assertion	dmmptdf	$$⊢\phi \to \mathrm{dom}A=B$$

Proof

Step	Hyp	Ref	Expression
1		dmmptdf.x	$$⊢Ⅎx\phi$$
2		dmmptdf.a	$$⊢A=\left(x\in B⟼C\right)$$
3		dmmptdf.c	$$⊢\left(\phi \wedge x\in B\right)\to C\in V$$
4		nfcv	$$⊢\underset{\_}{Ⅎ}xB$$
5	1 4 2 3	dmmptdff	$$⊢\phi \to \mathrm{dom}A=B$$