Metamath Proof Explorer

Theorem dmresexg

Description: The domain of a restriction to a set exists. (Contributed by NM, 7-Apr-1995)

Ref Expression
Assertion dmresexg B V dom A B V


Step Hyp Ref Expression
1 dmres dom A B = B dom A
2 inex1g B V B dom A V
3 1 2 eqeltrid B V dom A B V