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		nfcv	|- F/_ x B
5	1 4 2 3	dmmptdff	|- ( ph -> dom A = B )