Description: Weak version of ax-10 from which we can prove any ax-10 instance not involving wff variables or bundling. Uses only Tarski's FOL axiom schemes. It is an alias of hbn1w introduced for labeling consistency. (Contributed by NM, 9-Apr-2017) Use hbn1w instead. (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | ax10w.1 | |- ( x = y -> ( ph <-> ps ) ) |
|
| Assertion | ax10w | |- ( -. A. x ph -> A. x -. A. x ph ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax10w.1 | |- ( x = y -> ( ph <-> ps ) ) |
|
| 2 | 1 | hbn1w | |- ( -. A. x ph -> A. x -. A. x ph ) |