Description: Change bound variable in a restricted description binder. Version of cbvriotav with a disjoint variable condition, which requires fewer axioms . (Contributed by NM, 18-Mar-2013) (Revised by Gino Giotto, 30-Sep-2024)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | cbvriotavw.1 | |- ( x = y -> ( ph <-> ps ) ) |
|
| Assertion | cbvriotavw | |- ( iota_ x e. A ph ) = ( iota_ y e. A ps ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cbvriotavw.1 | |- ( x = y -> ( ph <-> ps ) ) |
|
| 2 | eleq1w | |- ( x = y -> ( x e. A <-> y e. A ) ) |
|
| 3 | 2 1 | anbi12d | |- ( x = y -> ( ( x e. A /\ ph ) <-> ( y e. A /\ ps ) ) ) |
| 4 | 3 | cbviotavw | |- ( iota x ( x e. A /\ ph ) ) = ( iota y ( y e. A /\ ps ) ) |
| 5 | df-riota | |- ( iota_ x e. A ph ) = ( iota x ( x e. A /\ ph ) ) |
|
| 6 | df-riota | |- ( iota_ y e. A ps ) = ( iota y ( y e. A /\ ps ) ) |
|
| 7 | 4 5 6 | 3eqtr4i | |- ( iota_ x e. A ph ) = ( iota_ y e. A ps ) |