This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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	$⊢ \neg \forall x x = y \to \forall z \neg \forall x x = y$

Proof

Step	Hyp	Ref	Expression
1		naev2	$⊢ \neg \forall x x = y \to \forall z \neg \forall x x = y$