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\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}B=C\leftrightarrow ⦋A/x⦌B=⦋A/x⦌C\right)$$

Proof

Step	Hyp	Ref	Expression
1		dfsbcq2	$$⊢z=A\to \left(\left[z/x\right]B=C\leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}B=C\right)$$
2		dfsbcq2	$$⊢z=A\to \left(\left[z/x\right]y\in B\leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in B\right)$$
3	2	abbidv	$$⊢z=A\to \left\{y|\left[z/x\right]y\in B\right\}=\left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in B\right\}$$
4		dfsbcq2	$$⊢z=A\to \left(\left[z/x\right]y\in C\leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in C\right)$$
5	4	abbidv	$$⊢z=A\to \left\{y|\left[z/x\right]y\in C\right\}=\left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in C\right\}$$
6	3 5	eqeq12d	$$⊢z=A\to \left(\left\{y|\left[z/x\right]y\in B\right\}=\left\{y|\left[z/x\right]y\in C\right\}\leftrightarrow \left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in B\right\}=\left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in C\right\}\right)$$
7		nfs1v	$$⊢Ⅎx\left[z/x\right]y\in B$$
8	7	nfab	$$⊢\underset{\_}{Ⅎ}x\left\{y|\left[z/x\right]y\in B\right\}$$
9		nfs1v	$$⊢Ⅎx\left[z/x\right]y\in C$$
10	9	nfab	$$⊢\underset{\_}{Ⅎ}x\left\{y|\left[z/x\right]y\in C\right\}$$
11	8 10	nfeq	$$⊢Ⅎx\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\leftrightarrow \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\leftrightarrow \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	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}B=C\leftrightarrow \left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in B\right\}=\left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in C\right\}\right)$$
17		df-csb	$$⊢⦋A/x⦌B=\left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in B\right\}$$
18		df-csb	$$⊢⦋A/x⦌C=\left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in C\right\}$$
19	17 18	eqeq12i	$$⊢⦋A/x⦌B=⦋A/x⦌C\leftrightarrow \left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in B\right\}=\left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in C\right\}$$
20	16 19	bitr4di	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}B=C\leftrightarrow ⦋A/x⦌B=⦋A/x⦌C\right)$$