Metamath Proof Explorer


Theorem cbvmptfg

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. Usage of this theorem is discouraged because it depends on ax-13 . See cbvmptf for a version with more disjoint variable conditions, but not requiring ax-13 . (Contributed by NM, 11-Sep-2011) (Revised by Thierry Arnoux, 9-Mar-2017) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 cbvmptfg.1
 |-  F/_ x A
2 cbvmptfg.2
 |-  F/_ y A
3 cbvmptfg.3
 |-  F/_ y B
4 cbvmptfg.4
 |-  F/_ x C
5 cbvmptfg.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 cbvopab1g
 |-  { <. 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 nfsb
 |-  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 sbie
 |-  ( [ 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 cbvopab1g
 |-  { <. 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 )