Theorem sbcbr12g

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

	Ref	Expression
Assertion	sbcbr12g	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}BRC\leftrightarrow ⦋A/x⦌BR⦋A/x⦌C\right)$$

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 V\to ⦋A/x⦌R=R$$
3	2	breqd	$$⊢A\in V\to \left(⦋A/x⦌B⦋A/x⦌R⦋A/x⦌C\leftrightarrow ⦋A/x⦌BR⦋A/x⦌C\right)$$
4	1 3	bitrid	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}BRC\leftrightarrow ⦋A/x⦌BR⦋A/x⦌C\right)$$