Description: Bound-variable hypothesis builder for substitution. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by Mario Carneiro, 4-Oct-2016) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | nfsb2 | |- ( -. A. x x = y -> F/ x [ y / x ] ph ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nfna1 | |- F/ x -. A. x x = y |
|
| 2 | hbsb2 | |- ( -. A. x x = y -> ( [ y / x ] ph -> A. x [ y / x ] ph ) ) |
|
| 3 | 1 2 | nf5d | |- ( -. A. x x = y -> F/ x [ y / x ] ph ) |