Metamath Proof Explorer


Theorem hbnaev

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 ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑧 ¬ ∀ 𝑥 𝑥 = 𝑦 )

Proof

Step Hyp Ref Expression
1 naev2 ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ∀ 𝑧 ¬ ∀ 𝑥 𝑥 = 𝑦 )