Theorem dmmptif

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

	Ref	Expression
Hypotheses	dmmptif.1	⊢ Ⅎ 𝑥 𝐴
	dmmptif.2	⊢ 𝐵 ∈ V
	dmmptif.3	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
Assertion	dmmptif	⊢ dom 𝐹 = 𝐴

Proof

Step	Hyp	Ref	Expression
1		dmmptif.1	⊢ Ⅎ 𝑥 𝐴
2		dmmptif.2	⊢ 𝐵 ∈ V
3		dmmptif.3	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
4	1 2 3	fnmptif	⊢ 𝐹 Fn 𝐴
5		fndm	⊢ ( 𝐹 Fn 𝐴 → dom 𝐹 = 𝐴 )
6	4 5	ax-mp	⊢ dom 𝐹 = 𝐴