Metamath Proof Explorer

Theorem resiexg

Description: The existence of a restricted identity function, proved without using the Axiom of Replacement (unlike resfunexg ). (Contributed by NM, 13-Jan-2007) (Proof shortened by Peter Mazsa, 2-Oct-2022)

Ref Expression
Assertion resiexg A V I A V


Step Hyp Ref Expression
1 idssxp I A A × A
2 sqxpexg A V A × A V
3 ssexg I A A × A A × A V I A V
4 1 2 3 sylancr A V I A V