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 ax-13 . See cbvmptvg for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 17-Jan-2024)

Ref Expression
Hypothesis cbvmptv.1 x = y B = C
Assertion cbvmptv x A B = y A C

Proof

Step Hyp Ref Expression
1 cbvmptv.1 x = y B = C
2 nfcv _ y B
3 nfcv _ x C
4 2 3 1 cbvmpt x A B = y A C