Theorem residm

Description: Idempotent law for restriction. (Contributed by NM, 27-Mar-1998)

	Ref	Expression
Assertion	residm	$$⊢{\left({A\upharpoonright }_B\right)\upharpoonright }_B={A\upharpoonright }_B$$

Proof

Step	Hyp	Ref	Expression
1		ssid	$$⊢B\subseteq B$$
2		resabs2	$$⊢B\subseteq B\to {\left({A\upharpoonright }_B\right)\upharpoonright }_B={A\upharpoonright }_B$$
3	1 2	ax-mp	$$⊢{\left({A\upharpoonright }_B\right)\upharpoonright }_B={A\upharpoonright }_B$$