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\in V\to {\mathrm{I}\upharpoonright }_A\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		idssxp	$$⊢{\mathrm{I}\upharpoonright }_A\subseteq A\times A$$
2		sqxpexg	$$⊢A\in V\to A\times A\in \mathrm{V}$$
3		ssexg	$$⊢\left({\mathrm{I}\upharpoonright }_A\subseteq A\times A\wedge A\times A\in \mathrm{V}\right)\to {\mathrm{I}\upharpoonright }_A\in \mathrm{V}$$
4	1 2 3	sylancr	$$⊢A\in V\to {\mathrm{I}\upharpoonright }_A\in \mathrm{V}$$