Description: Change bounded variables in a special case. The reverse direction seems to involve ax-11 . My hope is that I will in some future be able to prove mo3 with reversed quantifiers not using ax-11 . See also the remark in mo4 , which lead me to this effort. (Contributed by Wolf Lammen, 5-Mar-2024)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | wl-cbvalsbi | |- ( A. x ph -> A. y [ y / x ] ph ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | stdpc4 | |- ( A. x ph -> [ y / x ] ph ) |
|
| 2 | 1 | alrimiv | |- ( A. x ph -> A. y [ y / x ] ph ) |