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	⊢ ( 𝐴 ∈ 𝑉 → ( I ↾ 𝐴 ) ∈ V )

Proof

Step	Hyp	Ref	Expression
1		idssxp	⊢ ( I ↾ 𝐴 ) ⊆ ( 𝐴 × 𝐴 )
2		sqxpexg	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 × 𝐴 ) ∈ V )
3		ssexg	⊢ ( ( ( I ↾ 𝐴 ) ⊆ ( 𝐴 × 𝐴 ) ∧ ( 𝐴 × 𝐴 ) ∈ V ) → ( I ↾ 𝐴 ) ∈ V )
4	1 2 3	sylancr	⊢ ( 𝐴 ∈ 𝑉 → ( I ↾ 𝐴 ) ∈ V )