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	$⊢ A \in V \to {I ↾}_{A} \in V$

Proof

Step	Hyp	Ref	Expression
1		idssxp	$⊢ {I ↾}_{A} \subseteq A \times A$
2		sqxpexg	$⊢ A \in V \to A \times A \in V$
3		ssexg	$⊢ ({I ↾}_{A} \subseteq A \times A \land A \times A \in V) \to {I ↾}_{A} \in V$
4	1 2 3	sylancr	$⊢ A \in V \to {I ↾}_{A} \in V$