Theorem dmmptdf2

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

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

Proof

Step	Hyp	Ref	Expression
1		dmmptdf2.x	$$⊢Ⅎx\phi$$
2		dmmptdf2.b	$$⊢\underset{\_}{Ⅎ}xB$$
3		dmmptdf2.a	$$⊢A=\left(x\in B⟼C\right)$$
4		dmmptdf2.c	$$⊢\left(\phi \wedge x\in B\right)\to C\in V$$
5	3	dmmpt	$$⊢\mathrm{dom}A=\left\{x\in B|C\in \mathrm{V}\right\}$$
6	4	elexd	$$⊢\left(\phi \wedge x\in B\right)\to C\in \mathrm{V}$$
7	1 6	ralrimia	$$⊢\phi \to \forall x\in BC\in \mathrm{V}$$
8	2	rabid2f	$$⊢B=\left\{x\in B|C\in \mathrm{V}\right\}\leftrightarrow \forall x\in BC\in \mathrm{V}$$
9	7 8	sylibr	$$⊢\phi \to B=\left\{x\in B|C\in \mathrm{V}\right\}$$
10	5 9	eqtr4id	$$⊢\phi \to \mathrm{dom}A=B$$