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 ⊢ Ⅎ x φ
dmmptdf.a ⊢ A = x ∈ B ⟼ C
dmmptdf.c ⊢ φ ∧ x ∈ B → C ∈ V
Assertion dmmptdf ⊢ φ → dom ⁡ A = B

Proof

Step Hyp Ref Expression
1 dmmptdf.x ⊢ Ⅎ x φ
2 dmmptdf.a ⊢ A = x ∈ B ⟼ C
3 dmmptdf.c ⊢ φ ∧ x ∈ B → C ∈ V
4 nfcv ⊢ Ⅎ _ x B
5 1 4 2 3 dmmptdff ⊢ φ → dom ⁡ A = B