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 B
2 resabs2 B B A B B = A B
3 1 2 ax-mp A B B = A B