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

Metamath Proof Explorer

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 ) )