Theorem dmmptdf2

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

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

Proof

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