Metamath Proof Explorer

Theorem dmresi

Description: The domain of a restricted identity function. (Contributed by NM, 27-Aug-2004)

Ref Expression
Assertion dmresi dom I A = A


Step Hyp Ref Expression
1 ssv A V
2 dmi dom I = V
3 1 2 sseqtrri A dom I
4 ssdmres A dom I dom I A = A
5 3 4 mpbi dom I A = A