Metamath Proof Explorer

Theorem dmresv

Description: The domain of a universal restriction. (Contributed by NM, 14-May-2008)

Ref Expression
Assertion dmresv 
|- dom ( A |` _V ) = dom A

Proof

Step Hyp Ref Expression
1 dmres 
 |-  dom ( A |` _V ) = ( _V i^i dom A )
2 incom 
 |-  ( _V i^i dom A ) = ( dom A i^i _V )
3 inv1 
 |-  ( dom A i^i _V ) = dom A
4 1 2 3 3eqtri 
 |-  dom ( A |` _V ) = dom A