This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) = 𝐵 )