Theorem dmmptif

Description: Domain of the mapping operation. (Contributed by Glauco Siliprandi, 21-Dec-2024)

	Ref	Expression
Hypotheses	dmmptif.1	|- F/_ x A
	dmmptif.2	|- B e. _V
	dmmptif.3	|- F = ( x e. A |-> B )
Assertion	dmmptif	|- dom F = A

Proof

Step	Hyp	Ref	Expression
1		dmmptif.1	|- F/_ x A
2		dmmptif.2	|- B e. _V
3		dmmptif.3	|- F = ( x e. A |-> B )
4	1 2 3	fnmptif	|- F Fn A
5		fndm	|- ( F Fn A -> dom F = A )
6	4 5	ax-mp	|- dom F = A