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

Metamath Proof Explorer

Theorem dmeqi

Description: Equality inference for domain. (Contributed by NM, 4-Mar-2004)

Ref Expression
Hypothesis dmeqi.1 ⊢ A = B
Assertion dmeqi ⊢ dom ⁡ A = dom ⁡ B

Proof

Step Hyp Ref Expression
1 dmeqi.1 ⊢ A = B
2 dmeq ⊢ A = B → dom ⁡ A = dom ⁡ B
3 1 2 ax-mp ⊢ dom ⁡ A = dom ⁡ B