Theorem sbceq2g

Description: Move proper substitution to second argument of an equality. (Contributed by NM, 30-Nov-2005)

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

Proof

Step	Hyp	Ref	Expression
1		sbceqg	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}B=C\leftrightarrow ⦋A/x⦌B=⦋A/x⦌C\right)$$
2		csbconstg	$$⊢A\in V\to ⦋A/x⦌B=B$$
3	2	eqeq1d	$$⊢A\in V\to \left(⦋A/x⦌B=⦋A/x⦌C\leftrightarrow B=⦋A/x⦌C\right)$$
4	1 3	bitrd	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}B=C\leftrightarrow B=⦋A/x⦌C\right)$$