Theorem resmptf

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

	Ref	Expression
Hypotheses	resmptf.a	|- F/_ x A
	resmptf.b	|- F/_ x B
Assertion	resmptf	|- ( B C_ A -> ( ( x e. A |-> C ) |` B ) = ( x e. B |-> C ) )

Proof

Step	Hyp	Ref	Expression
1		resmptf.a	|- F/_ x A
2		resmptf.b	|- F/_ x B
3		resmpt	|- ( B C_ A -> ( ( y e. A |-> [_ y / x ]_ C ) |` B ) = ( y e. B |-> [_ y / x ]_ C ) )
4		nfcv	|- F/_ y A
5		nfcv	|- F/_ y C
6		nfcsb1v	|- F/_ x [_ y / x ]_ C
7		csbeq1a	|- ( x = y -> C = [_ y / x ]_ C )
8	1 4 5 6 7	cbvmptf	|- ( x e. A |-> C ) = ( y e. A |-> [_ y / x ]_ C )
9	8	reseq1i	|- ( ( x e. A |-> C ) |` B ) = ( ( y e. A |-> [_ y / x ]_ C ) |` B )
10		nfcv	|- F/_ y B
11	2 10 5 6 7	cbvmptf	|- ( x e. B |-> C ) = ( y e. B |-> [_ y / x ]_ C )
12	3 9 11	3eqtr4g	|- ( B C_ A -> ( ( x e. A |-> C ) |` B ) = ( x e. B |-> C ) )