Metamath Proof Explorer

Theorem sbceq1a

Description: Equality theorem for class substitution. Class version of sbequ12 . (Contributed by NM, 26-Sep-2003)

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

Proof

Step Hyp Ref Expression
1 sbid 
 |-  ( [ x / x ] ph <-> ph )
2 dfsbcq2 
 |-  ( x = A -> ( [ x / x ] ph <-> [. A / x ]. ph ) )
3 1 2 bitr3id 
 |-  ( x = A -> ( ph <-> [. A / x ]. ph ) )