Metamath Proof Explorer


Theorem sbceqbid

Description: Equality theorem for class substitution. (Contributed by Thierry Arnoux, 4-Sep-2018)

Ref Expression
Hypotheses sbceqbid.1
|- ( ph -> A = B )
sbceqbid.2
|- ( ph -> ( ps <-> ch ) )
Assertion sbceqbid
|- ( ph -> ( [. A / x ]. ps <-> [. B / x ]. ch ) )

Proof

Step Hyp Ref Expression
1 sbceqbid.1
 |-  ( ph -> A = B )
2 sbceqbid.2
 |-  ( ph -> ( ps <-> ch ) )
3 2 abbidv
 |-  ( ph -> { x | ps } = { x | ch } )
4 1 3 eleq12d
 |-  ( ph -> ( A e. { x | ps } <-> B e. { x | ch } ) )
5 df-sbc
 |-  ( [. A / x ]. ps <-> A e. { x | ps } )
6 df-sbc
 |-  ( [. B / x ]. ch <-> B e. { x | ch } )
7 4 5 6 3bitr4g
 |-  ( ph -> ( [. A / x ]. ps <-> [. B / x ]. ch ) )