Theorem dmmpt1

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

	Ref	Expression
Hypotheses	dmmpt1.x	⊢ Ⅎ 𝑥 𝜑
	dmmpt1.1	⊢ Ⅎ 𝑥 𝐵
	dmmpt1.c	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐶 ∈ 𝑉 )
Assertion	dmmpt1	⊢ ( 𝜑 → dom ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		dmmpt1.x	⊢ Ⅎ 𝑥 𝜑
2		dmmpt1.1	⊢ Ⅎ 𝑥 𝐵
3		dmmpt1.c	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐶 ∈ 𝑉 )
4		eqid	⊢ ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑥 ∈ 𝐵 ↦ 𝐶 )
5	1 2 4 3	dmmptdff	⊢ ( 𝜑 → dom ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) = 𝐵 )