Theorem dmmpti

Description: Domain of the mapping operation. (Contributed by NM, 6-Sep-2005) (Revised by Mario Carneiro, 31-Aug-2015)

	Ref	Expression
Hypotheses	fnmpti.1	⊢ 𝐵 ∈ V
	fnmpti.2	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
Assertion	dmmpti	⊢ dom 𝐹 = 𝐴

Proof

Step	Hyp	Ref	Expression
1		fnmpti.1	⊢ 𝐵 ∈ V
2		fnmpti.2	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
3	1 2	fnmpti	⊢ 𝐹 Fn 𝐴
4	3	fndmi	⊢ dom 𝐹 = 𝐴