Metamath Proof Explorer

Theorem resdmss

Description: Subset relationship for the domain of a restriction. (Contributed by Scott Fenton, 9-Aug-2024)

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

Proof

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