# 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
`|- F/_ y C`
cbvcsb.2
`|- F/_ x D`
cbvcsb.3
`|- ( x = y -> C = D )`
Assertion cbvcsb
`|- [_ A / x ]_ C = [_ A / y ]_ D`

### Proof

Step Hyp Ref Expression
1 cbvcsb.1
` |-  F/_ y C`
2 cbvcsb.2
` |-  F/_ x D`
3 cbvcsb.3
` |-  ( x = y -> C = D )`
4 1 nfcri
` |-  F/ y z e. C`
5 2 nfcri
` |-  F/ x z e. D`
6 3 eleq2d
` |-  ( x = y -> ( z e. C <-> z e. D ) )`
7 4 5 6 cbvsbc
` |-  ( [. A / x ]. z e. C <-> [. A / y ]. z e. D )`
8 7 abbii
` |-  { z | [. A / x ]. z e. C } = { z | [. A / y ]. z e. D }`
9 df-csb
` |-  [_ A / x ]_ C = { z | [. A / x ]. z e. C }`
10 df-csb
` |-  [_ A / y ]_ D = { z | [. A / y ]. z e. D }`
11 8 9 10 3eqtr4i
` |-  [_ A / x ]_ C = [_ A / y ]_ D`