Metamath Proof Explorer

Theorem resmpt3

Description: Unconditional restriction of the mapping operation. (Contributed by Stefan O'Rear, 24-Jan-2015) (Proof shortened by Mario Carneiro, 22-Mar-2015)

Ref Expression
Assertion resmpt3 
|- ( ( x e. A |-> C ) |` B ) = ( x e. ( A i^i B ) |-> C )

Proof

Step Hyp Ref Expression
1 resres 
 |-  ( ( ( x e. A |-> C ) |` A ) |` B ) = ( ( x e. A |-> C ) |` ( A i^i B ) )
2 ssid 
 |-  A C_ A
3 resmpt 
 |-  ( A C_ A -> ( ( x e. A |-> C ) |` A ) = ( x e. A |-> C ) )
4 2 3 ax-mp 
 |-  ( ( x e. A |-> C ) |` A ) = ( x e. A |-> C )
5 4 reseq1i 
 |-  ( ( ( x e. A |-> C ) |` A ) |` B ) = ( ( x e. A |-> C ) |` B )
6 inss1 
 |-  ( A i^i B ) C_ A
7 resmpt 
 |-  ( ( A i^i B ) C_ A -> ( ( x e. A |-> C ) |` ( A i^i B ) ) = ( x e. ( A i^i B ) |-> C ) )
8 6 7 ax-mp 
 |-  ( ( x e. A |-> C ) |` ( A i^i B ) ) = ( x e. ( A i^i B ) |-> C )
9 1 5 8 3eqtr3i 
 |-  ( ( x e. A |-> C ) |` B ) = ( x e. ( A i^i B ) |-> C )