Metamath Proof Explorer


Theorem cbvcsbdavw2

Description: Change bound variable of a proper substitution into a class. General version of cbvcsbdavw . Deduction form. (Contributed by GG, 14-Aug-2025)

Ref Expression
Hypotheses cbvcsbdavw2.1 φ A = B
cbvcsbdavw2.2 φ x = y C = D
Assertion cbvcsbdavw2 φ A / x C = B / y D

Proof

Step Hyp Ref Expression
1 cbvcsbdavw2.1 φ A = B
2 cbvcsbdavw2.2 φ x = y C = D
3 2 eleq2d φ x = y t C t D
4 1 3 cbvsbcdavw2 φ [˙A / x]˙ t C [˙B / y]˙ t D
5 4 abbidv φ t | [˙A / x]˙ t C = t | [˙B / y]˙ t D
6 df-csb A / x C = t | [˙A / x]˙ t C
7 df-csb B / y D = t | [˙B / y]˙ t D
8 5 6 7 3eqtr4g φ A / x C = B / y D