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

Metamath Proof Explorer

Theorem cbvmptv

Description: Rule to change the bound variable in a maps-to function, using implicit substitution. (Contributed by Mario Carneiro, 19-Feb-2013) Add disjoint variable condition to avoid auxiliary axioms . See cbvmptvg for a less restrictive version requiring more axioms. (Revised by GG, 17-Nov-2024)

Ref Expression
Hypothesis cbvmptv.1 
|- ( x = y -> B = C )
Assertion cbvmptv 
|- ( x e. A |-> B ) = ( y e. A |-> C )

Proof

Step Hyp Ref Expression
1 cbvmptv.1 
 |-  ( x = y -> B = C )
2 eleq1w 
 |-  ( x = y -> ( x e. A <-> y e. A ) )
3 1 eqeq2d 
 |-  ( x = y -> ( z = B <-> z = C ) )
4 2 3 anbi12d 
 |-  ( x = y -> ( ( x e. A /\ z = B ) <-> ( y e. A /\ z = C ) ) )
5 4 cbvopab1v 
 |-  { <. x , z >. | ( x e. A /\ z = B ) } = { <. y , z >. | ( y e. A /\ z = C ) }
6 df-mpt 
 |-  ( x e. A |-> B ) = { <. x , z >. | ( x e. A /\ z = B ) }
7 df-mpt 
 |-  ( y e. A |-> C ) = { <. y , z >. | ( y e. A /\ z = C ) }
8 5 6 7 3eqtr4i 
 |-  ( x e. A |-> B ) = ( y e. A |-> C )