# Metamath Proof Explorer

## Theorem sbceqg

Description: Distribute proper substitution through an equality relation. (Contributed by NM, 10-Nov-2005) (Proof shortened by Andrew Salmon, 29-Jun-2011)

Ref Expression
Assertion sbceqg
`|- ( A e. V -> ( [. A / x ]. B = C <-> [_ A / x ]_ B = [_ A / x ]_ C ) )`

### Proof

Step Hyp Ref Expression
1 dfsbcq2
` |-  ( z = A -> ( [ z / x ] B = C <-> [. A / x ]. B = C ) )`
2 dfsbcq2
` |-  ( z = A -> ( [ z / x ] y e. B <-> [. A / x ]. y e. B ) )`
3 2 abbidv
` |-  ( z = A -> { y | [ z / x ] y e. B } = { y | [. A / x ]. y e. B } )`
4 dfsbcq2
` |-  ( z = A -> ( [ z / x ] y e. C <-> [. A / x ]. y e. C ) )`
5 4 abbidv
` |-  ( z = A -> { y | [ z / x ] y e. C } = { y | [. A / x ]. y e. C } )`
6 3 5 eqeq12d
` |-  ( z = A -> ( { y | [ z / x ] y e. B } = { y | [ z / x ] y e. C } <-> { y | [. A / x ]. y e. B } = { y | [. A / x ]. y e. C } ) )`
7 nfs1v
` |-  F/ x [ z / x ] y e. B`
8 7 nfab
` |-  F/_ x { y | [ z / x ] y e. B }`
9 nfs1v
` |-  F/ x [ z / x ] y e. C`
10 9 nfab
` |-  F/_ x { y | [ z / x ] y e. C }`
11 8 10 nfeq
` |-  F/ x { y | [ z / x ] y e. B } = { y | [ z / x ] y e. C }`
12 sbab
` |-  ( x = z -> B = { y | [ z / x ] y e. B } )`
13 sbab
` |-  ( x = z -> C = { y | [ z / x ] y e. C } )`
14 12 13 eqeq12d
` |-  ( x = z -> ( B = C <-> { y | [ z / x ] y e. B } = { y | [ z / x ] y e. C } ) )`
15 11 14 sbiev
` |-  ( [ z / x ] B = C <-> { y | [ z / x ] y e. B } = { y | [ z / x ] y e. C } )`
16 1 6 15 vtoclbg
` |-  ( A e. V -> ( [. A / x ]. B = C <-> { y | [. A / x ]. y e. B } = { y | [. A / x ]. y e. C } ) )`
17 df-csb
` |-  [_ A / x ]_ B = { y | [. A / x ]. y e. B }`
18 df-csb
` |-  [_ A / x ]_ C = { y | [. A / x ]. y e. C }`
19 17 18 eqeq12i
` |-  ( [_ A / x ]_ B = [_ A / x ]_ C <-> { y | [. A / x ]. y e. B } = { y | [. A / x ]. y e. C } )`
20 16 19 syl6bbr
` |-  ( A e. V -> ( [. A / x ]. B = C <-> [_ A / x ]_ B = [_ A / x ]_ C ) )`