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 ) ) |
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 ) ) |