Theorem sbcel12

Description: Distribute proper substitution through a membership relation. (Contributed by NM, 10-Nov-2005) (Revised by NM, 18-Aug-2018)

	Ref	Expression
Assertion	sbcel12	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}B\in C\leftrightarrow ⦋A/x⦌B\in ⦋A/x⦌C$$

Proof

Step	Hyp	Ref	Expression
1		dfsbcq2	$$⊢z=A\to \left(\left[z/x\right]B\in C\leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}B\in 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	eleq12d	$$⊢z=A\to \left(\left\{y|\left[z/x\right]y\in B\right\}\in \left\{y|\left[z/x\right]y\in C\right\}\leftrightarrow \left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in B\right\}\in \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	nfel	$$⊢Ⅎx\left\{y|\left[z/x\right]y\in B\right\}\in \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	eleq12d	$$⊢x=z\to \left(B\in C\leftrightarrow \left\{y|\left[z/x\right]y\in B\right\}\in \left\{y|\left[z/x\right]y\in C\right\}\right)$$
15	11 14	sbiev	$$⊢\left[z/x\right]B\in C\leftrightarrow \left\{y|\left[z/x\right]y\in B\right\}\in \left\{y|\left[z/x\right]y\in C\right\}$$
16	1 6 15	vtoclbg	$$⊢A\in \mathrm{V}\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}B\in C\leftrightarrow \left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in B\right\}\in \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	eleq12i	$$⊢⦋A/x⦌B\in ⦋A/x⦌C\leftrightarrow \left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in B\right\}\in \left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in C\right\}$$
20	16 19	bitr4di	$$⊢A\in \mathrm{V}\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}B\in C\leftrightarrow ⦋A/x⦌B\in ⦋A/x⦌C\right)$$
21		sbcex	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}B\in C\to A\in \mathrm{V}$$
22	21	con3i	$$⊢\neg A\in \mathrm{V}\to \neg \underset{\dot{}}{[}A/x\underset{\dot{}}{]}B\in C$$
23		noel	$$⊢\neg ⦋A/x⦌B\in \varnothing$$
24		csbprc	$$⊢\neg A\in \mathrm{V}\to ⦋A/x⦌C=\varnothing$$
25	24	eleq2d	$$⊢\neg A\in \mathrm{V}\to \left(⦋A/x⦌B\in ⦋A/x⦌C\leftrightarrow ⦋A/x⦌B\in \varnothing \right)$$
26	23 25	mtbiri	$$⊢\neg A\in \mathrm{V}\to \neg ⦋A/x⦌B\in ⦋A/x⦌C$$
27	22 26	2falsed	$$⊢\neg A\in \mathrm{V}\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}B\in C\leftrightarrow ⦋A/x⦌B\in ⦋A/x⦌C\right)$$
28	20 27	pm2.61i	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}B\in C\leftrightarrow ⦋A/x⦌B\in ⦋A/x⦌C$$