# 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

### Proof

Step Hyp Ref Expression
1 dfsbcq2
2 dfsbcq2
3 2 abbidv
4 dfsbcq2
5 4 abbidv
6 3 5 eqeq12d
7 nfs1v ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left[{z}/{x}\right]{y}\in {B}$
8 7 nfab ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left\{{y}|\left[{z}/{x}\right]{y}\in {B}\right\}$
9 nfs1v ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left[{z}/{x}\right]{y}\in {C}$
10 9 nfab ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left\{{y}|\left[{z}/{x}\right]{y}\in {C}\right\}$
11 8 10 nfeq ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left\{{y}|\left[{z}/{x}\right]{y}\in {B}\right\}=\left\{{y}|\left[{z}/{x}\right]{y}\in {C}\right\}$
12 sbab ${⊢}{x}={z}\to {B}=\left\{{y}|\left[{z}/{x}\right]{y}\in {B}\right\}$
13 sbab ${⊢}{x}={z}\to {C}=\left\{{y}|\left[{z}/{x}\right]{y}\in {C}\right\}$
14 12 13 eqeq12d ${⊢}{x}={z}\to \left({B}={C}↔\left\{{y}|\left[{z}/{x}\right]{y}\in {B}\right\}=\left\{{y}|\left[{z}/{x}\right]{y}\in {C}\right\}\right)$
15 11 14 sbiev ${⊢}\left[{z}/{x}\right]{B}={C}↔\left\{{y}|\left[{z}/{x}\right]{y}\in {B}\right\}=\left\{{y}|\left[{z}/{x}\right]{y}\in {C}\right\}$
16 1 6 15 vtoclbg
17 df-csb
18 df-csb
19 17 18 eqeq12i
20 16 19 syl6bbr