Metamath Proof Explorer

Theorem sbceq2a

Description: Equality theorem for class substitution. Class version of sbequ12r . (Contributed by NM, 4-Jan-2017)

Ref Expression
Assertion sbceq2a 
|- ( A = x -> ( [. A / x ]. ph <-> ph ) )

Proof

Step Hyp Ref Expression
1 sbceq1a 
 |-  ( x = A -> ( ph <-> [. A / x ]. ph ) )
2 1 eqcoms 
 |-  ( A = x -> ( ph <-> [. A / x ]. ph ) )
3 2 bicomd 
 |-  ( A = x -> ( [. A / x ]. ph <-> ph ) )