Metamath Proof Explorer

Theorem eqsb3

Description: Substitution applied to an atomic wff (class version of equsb3 ). (Contributed by Rodolfo Medina, 28-Apr-2010)

Ref Expression
Assertion eqsb3 
|- ( [ 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 )