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 e. V -> dom ( A |` B ) e. _V )

Proof

Step Hyp Ref Expression
1 dmres 
 |-  dom ( A |` B ) = ( B i^i dom A )
2 inex1g 
 |-  ( B e. V -> ( B i^i dom A ) e. _V )
3 1 2 eqeltrid 
 |-  ( B e. V -> dom ( A |` B ) e. _V )