Theorem dmmptdff

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

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

Proof

Step	Hyp	Ref	Expression
1		dmmptdff.x	|- F/ x ph
2		dmmptdff.1	|- F/_ x B
3		dmmptdff.a	|- A = ( x e. B |-> C )
4		dmmptdff.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 )