Theorem dmmptdf

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

	Ref	Expression
Hypotheses	dmmptdf.x	|- F/ x ph
	dmmptdf.a	|- A = ( x e. B |-> C )
	dmmptdf.c	|- ( ( ph /\ x e. B ) -> C e. V )
Assertion	dmmptdf	|- ( ph -> dom A = B )

Proof

Step	Hyp	Ref	Expression
1		dmmptdf.x	|- F/ x ph
2		dmmptdf.a	|- A = ( x e. B |-> C )
3		dmmptdf.c	|- ( ( ph /\ x e. B ) -> C e. V )
4	2	dmmpt	|- dom A = { x e. B | C e. _V }
5	3	elexd	|- ( ( ph /\ x e. B ) -> C e. _V )
6	1 5	ralrimia	|- ( ph -> A. x e. B C e. _V )
7		rabid2	|- ( B = { x e. B | C e. _V } <-> A. x e. B C e. _V )
8	6 7	sylibr	|- ( ph -> B = { x e. B | C e. _V } )
9	4 8	eqtr4id	|- ( ph -> dom A = B )