Metamath Proof Explorer

Theorem residm

Description: Idempotent law for restriction. (Contributed by NM, 27-Mar-1998)

Ref Expression
Assertion residm 
|- ( ( A |` B ) |` B ) = ( A |` B )

Proof

Step Hyp Ref Expression
1 ssid 
 |-  B C_ B
2 resabs2 
 |-  ( B C_ B -> ( ( A |` B ) |` B ) = ( A |` B ) )
3 1 2 ax-mp 
 |-  ( ( A |` B ) |` B ) = ( A |` B )