Theorem dmmptd

Description: The domain of the mapping operation, deduction form. (Contributed by Glauco Siliprandi, 11-Dec-2019)

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

Proof

Step	Hyp	Ref	Expression
1		dmmptd.a	$$⊢A=\left(x\in B⟼C\right)$$
2		dmmptd.c	$$⊢\left(\phi \wedge x\in B\right)\to C\in V$$
3	2	elexd	$$⊢\left(\phi \wedge x\in B\right)\to C\in \mathrm{V}$$
4	3	ralrimiva	$$⊢\phi \to \forall x\in BC\in \mathrm{V}$$
5		rabid2	$$⊢B=\left\{x\in B|C\in \mathrm{V}\right\}\leftrightarrow \forall x\in BC\in \mathrm{V}$$
6	4 5	sylibr	$$⊢\phi \to B=\left\{x\in B|C\in \mathrm{V}\right\}$$
7	1	dmmpt	$$⊢\mathrm{dom}A=\left\{x\in B|C\in \mathrm{V}\right\}$$
8	6 7	syl6reqr	$$⊢\phi \to \mathrm{dom}A=B$$