This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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