Metamath Proof Explorer

Theorem sbcbidv

Description: Formula-building deduction for class substitution. (Contributed by NM, 29-Dec-2014) Drop ax-12 . (Revised by GG, 1-Dec-2023)

Ref Expression
Hypothesis sbcbidv.1 
|- ( ph -> ( ps <-> ch ) )
Assertion sbcbidv 
|- ( ph -> ( [. A / x ]. ps <-> [. A / x ]. ch ) )

Proof

Step Hyp Ref Expression
1 sbcbidv.1 
 |-  ( ph -> ( ps <-> ch ) )
2 eqidd 
 |-  ( ph -> A = A )
3 2 1 sbceqbid 
 |-  ( ph -> ( [. A / x ]. ps <-> [. A / x ]. ch ) )