Description: Equality theorem for class substitution. (Contributed by Thierry Arnoux, 4-Sep-2018)
Ref | Expression | ||
---|---|---|---|
Hypotheses | sbceqbidf.1 | |- F/ x ph |
|
sbceqbidf.2 | |- ( ph -> A = B ) |
||
sbceqbidf.3 | |- ( ph -> ( ps <-> ch ) ) |
||
Assertion | sbceqbidf | |- ( ph -> ( [. A / x ]. ps <-> [. B / x ]. ch ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sbceqbidf.1 | |- F/ x ph |
|
2 | sbceqbidf.2 | |- ( ph -> A = B ) |
|
3 | sbceqbidf.3 | |- ( ph -> ( ps <-> ch ) ) |
|
4 | 1 3 | abbid | |- ( ph -> { x | ps } = { x | ch } ) |
5 | 2 4 | eleq12d | |- ( ph -> ( A e. { x | ps } <-> B e. { x | ch } ) ) |
6 | df-sbc | |- ( [. A / x ]. ps <-> A e. { x | ps } ) |
|
7 | df-sbc | |- ( [. B / x ]. ch <-> B e. { x | ch } ) |
|
8 | 5 6 7 | 3bitr4g | |- ( ph -> ( [. A / x ]. ps <-> [. B / x ]. ch ) ) |