Theorem dmmpt1

Description: The domain of the mapping operation, deduction form. (Contributed by Glauco Siliprandi, 5-Jan-2025)

	Ref	Expression
Hypotheses	dmmpt1.x	$$⊢Ⅎx\phi$$
	dmmpt1.1	$$⊢\underset{\_}{Ⅎ}xB$$
	dmmpt1.c	$$⊢\left(\phi \wedge x\in B\right)\to C\in V$$
Assertion	dmmpt1	$$⊢\phi \to \mathrm{dom}\left(x\in B⟼C\right)=B$$

Proof

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