Theorem sbcbr

Description: Move substitution in and out of a binary relation. (Contributed by NM, 23-Aug-2018)

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

Proof

Step	Hyp	Ref	Expression
1		sbcbr123	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}BRC\leftrightarrow ⦋A/x⦌B⦋A/x⦌R⦋A/x⦌C$$
2		csbconstg	$$⊢A\in \mathrm{V}\to ⦋A/x⦌B=B$$
3		csbconstg	$$⊢A\in \mathrm{V}\to ⦋A/x⦌C=C$$
4	2 3	breq12d	$$⊢A\in \mathrm{V}\to \left(⦋A/x⦌B⦋A/x⦌R⦋A/x⦌C\leftrightarrow B⦋A/x⦌RC\right)$$
5		br0	$$⊢\neg ⦋A/x⦌B\varnothing ⦋A/x⦌C$$
6		csbprc	$$⊢\neg A\in \mathrm{V}\to ⦋A/x⦌R=\varnothing$$
7	6	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)$$
8	5 7	mtbiri	$$⊢\neg A\in \mathrm{V}\to \neg ⦋A/x⦌B⦋A/x⦌R⦋A/x⦌C$$
9		br0	$$⊢\neg B\varnothing C$$
10	6	breqd	$$⊢\neg A\in \mathrm{V}\to \left(B⦋A/x⦌RC\leftrightarrow B\varnothing C\right)$$
11	9 10	mtbiri	$$⊢\neg A\in \mathrm{V}\to \neg B⦋A/x⦌RC$$
12	8 11	2falsed	$$⊢\neg A\in \mathrm{V}\to \left(⦋A/x⦌B⦋A/x⦌R⦋A/x⦌C\leftrightarrow B⦋A/x⦌RC\right)$$
13	4 12	pm2.61i	$$⊢⦋A/x⦌B⦋A/x⦌R⦋A/x⦌C\leftrightarrow B⦋A/x⦌RC$$
14	1 13	bitri	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}BRC\leftrightarrow B⦋A/x⦌RC$$