Metamath Proof Explorer

Theorem eqsbc3r

Description: eqsbc3 with setvar variable on right side of equals sign. (Contributed by Alan Sare, 24-Oct-2011) (Proof shortened by JJ, 7-Jul-2021)

Ref Expression
Assertion eqsbc3r 
|- ( A e. V -> ( [. A / x ]. B = x <-> B = A ) )

Proof

Step Hyp Ref Expression
1 eqsbc3 
 |-  ( 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 ) )