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

Metamath Proof Explorer

Theorem axc9

Description: Derive set.mm's original ax-c9 from the shorter ax-13 . Usage is discouraged to avoid uninformed ax-13 propagation. (Contributed by NM, 29-Nov-2015) (Revised by NM, 24-Dec-2015) (Proof shortened by Wolf Lammen, 29-Apr-2018) (New usage is discouraged.)

		Ref	Expression
	Assertion	axc9	$⊢ \neg \forall z z = x \to (\neg \forall z z = y \to (x = y \to \forall z x = y))$

Proof

Step	Hyp	Ref	Expression
1		nfeqf	$⊢ (\neg \forall z z = x \land \neg \forall z z = y) \to Ⅎ z x = y$
2	1	nf5rd	$⊢ (\neg \forall z z = x \land \neg \forall z z = y) \to (x = y \to \forall z x = y)$
3	2	ex	$⊢ \neg \forall z z = x \to (\neg \forall z z = y \to (x = y \to \forall z x = y))$