Metamath Proof Explorer


Theorem cbvcsbv

Description: Change the bound variable of a proper substitution into a class using implicit substitution. (Contributed by NM, 30-Sep-2008) (Revised by Mario Carneiro, 13-Oct-2016)

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

Proof

Step Hyp Ref Expression
1 cbvcsbv.1 x = y B = C
2 1 eleq2d x = y z B z C
3 2 cbvsbcvw [˙A / x]˙ z B [˙A / y]˙ z C
4 3 abbii z | [˙A / x]˙ z B = z | [˙A / y]˙ z C
5 df-csb A / x B = z | [˙A / x]˙ z B
6 df-csb A / y C = z | [˙A / y]˙ z C
7 4 5 6 3eqtr4i A / x B = A / y C