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	⊢ ( [ 𝑦 / 𝑥 ] 𝐴 = 𝐵 ↔ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 = ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		nfcsb1v	⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐴
2		nfcsb1v	⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐵
3	1 2	nfeq	⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐴 = ⦋ 𝑦 / 𝑥 ⦌ 𝐵
4		csbeq1a	⊢ ( 𝑥 = 𝑦 → 𝐴 = ⦋ 𝑦 / 𝑥 ⦌ 𝐴 )
5		csbeq1a	⊢ ( 𝑥 = 𝑦 → 𝐵 = ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
6	4 5	eqeq12d	⊢ ( 𝑥 = 𝑦 → ( 𝐴 = 𝐵 ↔ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 = ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) )
7	3 6	sbiev	⊢ ( [ 𝑦 / 𝑥 ] 𝐴 = 𝐵 ↔ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 = ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )