# Metamath Proof Explorer

## Theorem cbvcsb

Description: Change bound variables in a class substitution. Interestingly, this does not require any bound variable conditions on A . Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker cbvcsbw when possible. (Contributed by Jeff Hankins, 13-Sep-2009) (Revised by Mario Carneiro, 11-Dec-2016) (New usage is discouraged.)

Ref Expression
Hypotheses cbvcsb.1 ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{C}$
cbvcsb.2 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{D}$
cbvcsb.3 ${⊢}{x}={y}\to {C}={D}$
Assertion cbvcsb

### Proof

Step Hyp Ref Expression
1 cbvcsb.1 ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{C}$
2 cbvcsb.2 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{D}$
3 cbvcsb.3 ${⊢}{x}={y}\to {C}={D}$
4 1 nfcri ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{z}\in {C}$
5 2 nfcri ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{z}\in {D}$
6 3 eleq2d ${⊢}{x}={y}\to \left({z}\in {C}↔{z}\in {D}\right)$
7 4 5 6 cbvsbc
8 7 abbii
9 df-csb
10 df-csb
11 8 9 10 3eqtr4i