Description: Any variable is free in -. A. x x = y , if x and y are distinct. This condition is dropped in hbnae , at the expense of more axiom dependencies. Instance of naev2 . (Contributed by NM, 13-May-1993) (Revised by Wolf Lammen, 9-Apr-2021)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | hbnaev | |- ( -. A. x x = y -> A. z -. A. x x = y ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | naev2 | |- ( -. A. x x = y -> A. z -. A. x x = y ) |