Description: The setvar x is not free in [ y / x ] ph when x and y are distinct. (Contributed by Mario Carneiro, 11-Aug-2016) Shorten nfs1v and hbs1 combined. (Revised by Wolf Lammen, 28-Jul-2022)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | nfs1v | |- F/ x [ y / x ] ph |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | sb6 | |- ( [ y / x ] ph <-> A. x ( x = y -> ph ) ) |
|
| 2 | nfa1 | |- F/ x A. x ( x = y -> ph ) |
|
| 3 | 1 2 | nfxfr | |- F/ x [ y / x ] ph |