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

Metamath Proof Explorer

Theorem cbvmptf

Description: Rule to change the bound variable in a maps-to function, using implicit substitution. This version has bound-variable hypotheses in place of distinct variable conditions. (Contributed by NM, 11-Sep-2011) (Revised by Thierry Arnoux, 9-Mar-2017) Add disjoint variable condition to avoid ax-13 . See cbvmptfg for a less restrictive version requiring more axioms. (Revised by GG, 17-Jan-2024)

Ref Expression
Hypotheses cbvmptf.1 
|- F/_ x A
cbvmptf.2 
|- F/_ y A
cbvmptf.3 
|- F/_ y B
cbvmptf.4 
|- F/_ x C
cbvmptf.5 
|- ( x = y -> B = C )
Assertion cbvmptf 
|- ( x e. A |-> B ) = ( y e. A |-> C )

Proof

Step Hyp Ref Expression
1 cbvmptf.1 
 |-  F/_ x A
2 cbvmptf.2 
 |-  F/_ y A
3 cbvmptf.3 
 |-  F/_ y B
4 cbvmptf.4 
 |-  F/_ x C
5 cbvmptf.5 
 |-  ( x = y -> B = C )
6 nfv 
 |-  F/ w ( x e. A /\ z = B )
7 1 nfcri 
 |-  F/ x w e. A
8 nfs1v 
 |-  F/ x [ w / x ] z = B
9 7 8 nfan 
 |-  F/ x ( w e. A /\ [ w / x ] z = B )
10 eleq1w 
 |-  ( x = w -> ( x e. A <-> w e. A ) )
11 sbequ12 
 |-  ( x = w -> ( z = B <-> [ w / x ] z = B ) )
12 10 11 anbi12d 
 |-  ( x = w -> ( ( x e. A /\ z = B ) <-> ( w e. A /\ [ w / x ] z = B ) ) )
13 6 9 12 cbvopab1 
 |-  { <. x , z >. | ( x e. A /\ z = B ) } = { <. w , z >. | ( w e. A /\ [ w / x ] z = B ) }
14 2 nfcri 
 |-  F/ y w e. A
15 3 nfeq2 
 |-  F/ y z = B
16 15 nfsbv 
 |-  F/ y [ w / x ] z = B
17 14 16 nfan 
 |-  F/ y ( w e. A /\ [ w / x ] z = B )
18 nfv 
 |-  F/ w ( y e. A /\ z = C )
19 eleq1w 
 |-  ( w = y -> ( w e. A <-> y e. A ) )
20 sbequ 
 |-  ( w = y -> ( [ w / x ] z = B <-> [ y / x ] z = B ) )
21 4 nfeq2 
 |-  F/ x z = C
22 5 eqeq2d 
 |-  ( x = y -> ( z = B <-> z = C ) )
23 21 22 sbiev 
 |-  ( [ y / x ] z = B <-> z = C )
24 20 23 bitrdi 
 |-  ( w = y -> ( [ w / x ] z = B <-> z = C ) )
25 19 24 anbi12d 
 |-  ( w = y -> ( ( w e. A /\ [ w / x ] z = B ) <-> ( y e. A /\ z = C ) ) )
26 17 18 25 cbvopab1 
 |-  { <. w , z >. | ( w e. A /\ [ w / x ] z = B ) } = { <. y , z >. | ( y e. A /\ z = C ) }
27 13 26 eqtri 
 |-  { <. x , z >. | ( x e. A /\ z = B ) } = { <. y , z >. | ( y e. A /\ z = C ) }
28 df-mpt 
 |-  ( x e. A |-> B ) = { <. x , z >. | ( x e. A /\ z = B ) }
29 df-mpt 
 |-  ( y e. A |-> C ) = { <. y , z >. | ( y e. A /\ z = C ) }
30 27 28 29 3eqtr4i 
 |-  ( x e. A |-> B ) = ( y e. A |-> C )