Theorem sbcbr123

Description: Move substitution in and out of a binary relation. (Contributed by NM, 13-Dec-2005) (Revised by NM, 22-Aug-2018)

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

Proof

Step	Hyp	Ref	Expression
1		sbcex	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}BRC\to A\in \mathrm{V}$$
2		br0	$$⊢\neg ⦋A/x⦌B\varnothing ⦋A/x⦌C$$
3		csbprc	$$⊢\neg A\in \mathrm{V}\to ⦋A/x⦌R=\varnothing$$
4	3	breqd	$$⊢\neg A\in \mathrm{V}\to \left(⦋A/x⦌B⦋A/x⦌R⦋A/x⦌C\leftrightarrow ⦋A/x⦌B\varnothing ⦋A/x⦌C\right)$$
5	2 4	mtbiri	$$⊢\neg A\in \mathrm{V}\to \neg ⦋A/x⦌B⦋A/x⦌R⦋A/x⦌C$$
6	5	con4i	$$⊢⦋A/x⦌B⦋A/x⦌R⦋A/x⦌C\to A\in \mathrm{V}$$
7		dfsbcq2	$$⊢y=A\to \left(\left[y/x\right]BRC\leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}BRC\right)$$
8		csbeq1	$$⊢y=A\to ⦋y/x⦌B=⦋A/x⦌B$$
9		csbeq1	$$⊢y=A\to ⦋y/x⦌R=⦋A/x⦌R$$
10		csbeq1	$$⊢y=A\to ⦋y/x⦌C=⦋A/x⦌C$$
11	8 9 10	breq123d	$$⊢y=A\to \left(⦋y/x⦌B⦋y/x⦌R⦋y/x⦌C\leftrightarrow ⦋A/x⦌B⦋A/x⦌R⦋A/x⦌C\right)$$
12		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋y/x⦌B$$
13		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋y/x⦌R$$
14		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋y/x⦌C$$
15	12 13 14	nfbr	$$⊢Ⅎx⦋y/x⦌B⦋y/x⦌R⦋y/x⦌C$$
16		csbeq1a	$$⊢x=y\to B=⦋y/x⦌B$$
17		csbeq1a	$$⊢x=y\to R=⦋y/x⦌R$$
18		csbeq1a	$$⊢x=y\to C=⦋y/x⦌C$$
19	16 17 18	breq123d	$$⊢x=y\to \left(BRC\leftrightarrow ⦋y/x⦌B⦋y/x⦌R⦋y/x⦌C\right)$$
20	15 19	sbiev	$$⊢\left[y/x\right]BRC\leftrightarrow ⦋y/x⦌B⦋y/x⦌R⦋y/x⦌C$$
21	7 11 20	vtoclbg	$$⊢A\in \mathrm{V}\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}BRC\leftrightarrow ⦋A/x⦌B⦋A/x⦌R⦋A/x⦌C\right)$$
22	1 6 21	pm5.21nii	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}BRC\leftrightarrow ⦋A/x⦌B⦋A/x⦌R⦋A/x⦌C$$