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

Metamath Proof Explorer

Theorem dmresi

Description: The domain of a restricted identity function. (Contributed by NM, 27-Aug-2004)

		Ref	Expression
	Assertion	dmresi	$⊢ dom ({I ↾}_{A}) = A$

Step	Hyp	Ref	Expression
1		ssv	$⊢ A \subseteq V$
2		dmi	$⊢ dom I = V$
3	1 2	sseqtrri	$⊢ A \subseteq dom I$
4		ssdmres	$⊢ A \subseteq dom I \leftrightarrow dom ({I ↾}_{A}) = A$
5	3 4	mpbi	$⊢ dom ({I ↾}_{A}) = A$