Description: Substitution of variable in universal quantifier. Closed form of sb8f . (Contributed by Wolf Lammen, 27-Apr-2025)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | wl-sb8ft | |- ( A. x F/ y ph -> ( A. x ph <-> A. y [ y / x ] ph ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | sbft | |- ( F/ y ph -> ( [ x / y ] ph <-> ph ) ) |
|
| 2 | 1 | alimi | |- ( A. x F/ y ph -> A. x ( [ x / y ] ph <-> ph ) ) |
| 3 | albi | |- ( A. x ( [ x / y ] ph <-> ph ) -> ( A. x [ x / y ] ph <-> A. x ph ) ) |
|
| 4 | 2 3 | syl | |- ( A. x F/ y ph -> ( A. x [ x / y ] ph <-> A. x ph ) ) |
| 5 | wl-sb9v | |- ( A. x [ x / y ] ph <-> A. y [ y / x ] ph ) |
|
| 6 | 4 5 | bitr3di | |- ( A. x F/ y ph -> ( A. x ph <-> A. y [ y / x ] ph ) ) |