# Metamath Proof Explorer

## Theorem cbvcsbw

Description: Change bound variables in a class substitution. Interestingly, this does not require any bound variable conditions on A . Version of cbvcsb with a disjoint variable condition, which does not require ax-13 . (Contributed by Jeff Hankins, 13-Sep-2009) (Revised by Gino Giotto, 10-Jan-2024)

Ref Expression
Hypotheses cbvcsbw.1
`|- F/_ y C`
cbvcsbw.2
`|- F/_ x D`
cbvcsbw.3
`|- ( x = y -> C = D )`
Assertion cbvcsbw
`|- [_ A / x ]_ C = [_ A / y ]_ D`

### Proof

Step Hyp Ref Expression
1 cbvcsbw.1
` |-  F/_ y C`
2 cbvcsbw.2
` |-  F/_ x D`
3 cbvcsbw.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 cbvsbcw
` |-  ( [. 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`