Theorem dmmpt1

Description: The domain of the mapping operation, deduction form. (Contributed by Glauco Siliprandi, 5-Jan-2025)

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

Proof

Step	Hyp	Ref	Expression
1		dmmpt1.x	|- F/ x ph
2		dmmpt1.1	|- F/_ x B
3		dmmpt1.c	|- ( ( ph /\ x e. B ) -> C e. V )
4		eqid	|- ( x e. B |-> C ) = ( x e. B |-> C )
5	1 2 4 3	dmmptdff	|- ( ph -> dom ( x e. B |-> C ) = B )