# 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}\phantom{\rule{.4em}{0ex}}{\phi }$
dmmptdf.a ${⊢}{A}=\left({x}\in {B}⟼{C}\right)$
dmmptdf.c ${⊢}\left({\phi }\wedge {x}\in {B}\right)\to {C}\in {V}$
Assertion dmmptdf ${⊢}{\phi }\to \mathrm{dom}{A}={B}$

### Proof

Step Hyp Ref Expression
1 dmmptdf.x ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }$
2 dmmptdf.a ${⊢}{A}=\left({x}\in {B}⟼{C}\right)$
3 dmmptdf.c ${⊢}\left({\phi }\wedge {x}\in {B}\right)\to {C}\in {V}$
4 3 elexd ${⊢}\left({\phi }\wedge {x}\in {B}\right)\to {C}\in \mathrm{V}$
5 1 4 ralrimia ${⊢}{\phi }\to \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}{C}\in \mathrm{V}$
6 rabid2 ${⊢}{B}=\left\{{x}\in {B}|{C}\in \mathrm{V}\right\}↔\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}{C}\in \mathrm{V}$
7 5 6 sylibr ${⊢}{\phi }\to {B}=\left\{{x}\in {B}|{C}\in \mathrm{V}\right\}$
8 2 dmmpt ${⊢}\mathrm{dom}{A}=\left\{{x}\in {B}|{C}\in \mathrm{V}\right\}$
9 7 8 syl6reqr ${⊢}{\phi }\to \mathrm{dom}{A}={B}$