Theorem sbceq2g

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

	Ref	Expression
Assertion	sbceq2g	|- ( A e. V -> ( [. A / x ]. B = C <-> B = [_ A / x ]_ C ) )

Proof

Step	Hyp	Ref	Expression
1		sbceqg	|- ( A e. V -> ( [. A / x ]. B = C <-> [_ A / x ]_ B = [_ A / x ]_ C ) )
2		csbconstg	|- ( A e. V -> [_ A / x ]_ B = B )
3	2	eqeq1d	|- ( A e. V -> ( [_ A / x ]_ B = [_ A / x ]_ C <-> B = [_ A / x ]_ C ) )
4	1 3	bitrd	|- ( A e. V -> ( [. A / x ]. B = C <-> B = [_ A / x ]_ C ) )