Theorem eqsbc2

Description: Substitution for the right-hand side in an equality. (Contributed by Alan Sare, 24-Oct-2011) (Proof shortened by JJ, 7-Jul-2021)

	Ref	Expression
Assertion	eqsbc2	⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] 𝐵 = 𝑥 ↔ 𝐵 = 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		eqsbc1	⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] 𝑥 = 𝐵 ↔ 𝐴 = 𝐵 ) )
2		eqcom	⊢ ( 𝐵 = 𝑥 ↔ 𝑥 = 𝐵 )
3	2	sbcbii	⊢ ( [ 𝐴 / 𝑥 ] 𝐵 = 𝑥 ↔ [ 𝐴 / 𝑥 ] 𝑥 = 𝐵 )
4		eqcom	⊢ ( 𝐵 = 𝐴 ↔ 𝐴 = 𝐵 )
5	1 3 4	3bitr4g	⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] 𝐵 = 𝑥 ↔ 𝐵 = 𝐴 ) )