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	$$⊢\left[y/x\right]A=B\leftrightarrow ⦋y/x⦌A=⦋y/x⦌B$$

Proof

Step	Hyp	Ref	Expression
1		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋y/x⦌A$$
2		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋y/x⦌B$$
3	1 2	nfeq	$$⊢Ⅎx⦋y/x⦌A=⦋y/x⦌B$$
4		csbeq1a	$$⊢x=y\to A=⦋y/x⦌A$$
5		csbeq1a	$$⊢x=y\to B=⦋y/x⦌B$$
6	4 5	eqeq12d	$$⊢x=y\to \left(A=B\leftrightarrow ⦋y/x⦌A=⦋y/x⦌B\right)$$
7	3 6	sbiev	$$⊢\left[y/x\right]A=B\leftrightarrow ⦋y/x⦌A=⦋y/x⦌B$$