Theorem sbceq1g

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

	Ref	Expression
Assertion	sbceq1g	|- ( A e. V -> ( [. A / x ]. B = C <-> [_ A / x ]_ B = 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 ]_ C = C )
3	2	eqeq2d	|- ( A e. V -> ( [_ A / x ]_ B = [_ A / x ]_ C <-> [_ A / x ]_ B = C ) )
4	1 3	bitrd	|- ( A e. V -> ( [. A / x ]. B = C <-> [_ A / x ]_ B = C ) )