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 
|- ( A e. V -> ( [. A / x ]. B = x <-> B = A ) )

Proof

Step Hyp Ref Expression
1 eqsbc1 
 |-  ( A e. V -> ( [. A / x ]. x = B <-> A = B ) )
2 eqcom 
 |-  ( B = x <-> x = B )
3 2 sbcbii 
 |-  ( [. A / x ]. B = x <-> [. A / x ]. x = B )
4 eqcom 
 |-  ( B = A <-> A = B )
5 1 3 4 3bitr4g 
 |-  ( A e. V -> ( [. A / x ]. B = x <-> B = A ) )