Theorem resmptf

Description: Restriction of the mapping operation. (Contributed by Thierry Arnoux, 28-Mar-2017)

	Ref	Expression
Hypotheses	resmptf.a	$$⊢\underset{\_}{Ⅎ}xA$$
	resmptf.b	$$⊢\underset{\_}{Ⅎ}xB$$
Assertion	resmptf	$$⊢B\subseteq A\to {\left(x\in A⟼C\right)\upharpoonright }_B=\left(x\in B⟼C\right)$$

Proof

Step	Hyp	Ref	Expression
1		resmptf.a	$$⊢\underset{\_}{Ⅎ}xA$$
2		resmptf.b	$$⊢\underset{\_}{Ⅎ}xB$$
3		resmpt	$$⊢B\subseteq A\to {\left(y\in A⟼⦋y/x⦌C\right)\upharpoonright }_B=\left(y\in B⟼⦋y/x⦌C\right)$$
4		nfcv	$$⊢\underset{\_}{Ⅎ}yA$$
5		nfcv	$$⊢\underset{\_}{Ⅎ}yC$$
6		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋y/x⦌C$$
7		csbeq1a	$$⊢x=y\to C=⦋y/x⦌C$$
8	1 4 5 6 7	cbvmptf	$$⊢\left(x\in A⟼C\right)=\left(y\in A⟼⦋y/x⦌C\right)$$
9	8	reseq1i	$$⊢{\left(x\in A⟼C\right)\upharpoonright }_B={\left(y\in A⟼⦋y/x⦌C\right)\upharpoonright }_B$$
10		nfcv	$$⊢\underset{\_}{Ⅎ}yB$$
11	2 10 5 6 7	cbvmptf	$$⊢\left(x\in B⟼C\right)=\left(y\in B⟼⦋y/x⦌C\right)$$
12	3 9 11	3eqtr4g	$$⊢B\subseteq A\to {\left(x\in A⟼C\right)\upharpoonright }_B=\left(x\in B⟼C\right)$$