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 zz=x\to \left(\neg \forall zz=y\to \left(x=y\to \forall zx=y\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		nfeqf	$$⊢\left(\neg \forall zz=x\wedge \neg \forall zz=y\right)\to Ⅎzx=y$$
2	1	nf5rd	$$⊢\left(\neg \forall zz=x\wedge \neg \forall zz=y\right)\to \left(x=y\to \forall zx=y\right)$$
3	2	ex	$$⊢\neg \forall zz=x\to \left(\neg \forall zz=y\to \left(x=y\to \forall zx=y\right)\right)$$