Description: Change bound variables in a description binder. Version of cbviotav with a disjoint variable condition, which requires fewer axioms . (Contributed by Andrew Salmon, 1-Aug-2011) (Revised by Gino Giotto, 30-Sep-2024)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | cbviotavw.1 | |- ( x = y -> ( ph <-> ps ) ) |
|
| Assertion | cbviotavw | |- ( iota x ph ) = ( iota y ps ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cbviotavw.1 | |- ( x = y -> ( ph <-> ps ) ) |
|
| 2 | 1 | cbvabv | |- { x | ph } = { y | ps } |
| 3 | 2 | eqeq1i | |- ( { x | ph } = { z } <-> { y | ps } = { z } ) |
| 4 | 3 | abbii | |- { z | { x | ph } = { z } } = { z | { y | ps } = { z } } |
| 5 | 4 | unieqi | |- U. { z | { x | ph } = { z } } = U. { z | { y | ps } = { z } } |
| 6 | df-iota | |- ( iota x ph ) = U. { z | { x | ph } = { z } } |
|
| 7 | df-iota | |- ( iota y ps ) = U. { z | { y | ps } = { z } } |
|
| 8 | 5 6 7 | 3eqtr4i | |- ( iota x ph ) = ( iota y ps ) |