This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] 𝐵 = 𝑥 ↔ 𝐵 = 𝐴 ) )