Metamath Proof Explorer


Theorem dmmptd

Description: The domain of the mapping operation, deduction form. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses dmmptd.a A = x B C
dmmptd.c φ x B C V
Assertion dmmptd φ dom A = B

Proof

Step Hyp Ref Expression
1 dmmptd.a A = x B C
2 dmmptd.c φ x B C V
3 1 dmmpt dom A = x B | C V
4 2 elexd φ x B C V
5 4 ralrimiva φ 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 3 7 eqtr4id φ dom A = B