Theorem bj-sbeqALT

Description: Substitution in an equality (use the more general version bj-sbeq instead, without disjoint variable condition). (Contributed by BJ, 6-Oct-2018) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Assertion	bj-sbeqALT	|- ( [ y / x ] A = B <-> [_ y / x ]_ A = [_ y / x ]_ B )

Proof

Step	Hyp	Ref	Expression
1		nfcsb1v	|- F/_ x [_ y / x ]_ A
2		nfcsb1v	|- F/_ x [_ y / x ]_ B
3	1 2	nfeq	|- F/ x [_ y / x ]_ A = [_ y / x ]_ B
4		csbeq1a	|- ( x = y -> A = [_ y / x ]_ A )
5		csbeq1a	|- ( x = y -> B = [_ y / x ]_ B )
6	4 5	eqeq12d	|- ( x = y -> ( A = B <-> [_ y / x ]_ A = [_ y / x ]_ B ) )
7	3 6	sbiev	|- ( [ y / x ] A = B <-> [_ y / x ]_ A = [_ y / x ]_ B )