Metamath Proof Explorer

Theorem dmresss

Description: The domain of a restriction is a subset of the original domain. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Assertion dmresss 
|- dom ( A |` B ) C_ dom A

Proof

Step Hyp Ref Expression
1 dmres 
 |-  dom ( A |` B ) = ( B i^i dom A )
2 inss2 
 |-  ( B i^i dom A ) C_ dom A
3 1 2 eqsstri 
 |-  dom ( A |` B ) C_ dom A