Metamath Proof Explorer

Theorem eqsb1

Description: Substitution for the left-hand side in an equality. Class version of equsb3 . (Contributed by Rodolfo Medina, 28-Apr-2010)

Ref Expression
Assertion eqsb1 
|- ( [ y / x ] x = A <-> y = A )

Proof

Step Hyp Ref Expression
1 eqeq1 
 |-  ( x = w -> ( x = A <-> w = A ) )
2 eqeq1 
 |-  ( w = y -> ( w = A <-> y = A ) )
3 1 2 sbievw2 
 |-  ( [ y / x ] x = A <-> y = A )