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 3 elexd φ x B C V
5 1 4 ralrimia φ x B C V
6 rabid2 B = x B | C V x B C V
7 5 6 sylibr φ B = x B | C V
8 2 dmmpt dom A = x B | C V
9 7 8 syl6reqr φ dom A = B