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

Metamath Proof Explorer

Theorem dmmptdf

Description: The domain of the mapping operation, deduction form. (Contributed by Glauco Siliprandi, 26-Jun-2021)

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

Proof

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