Theorem ax13fromc9

Description: Derive ax-13 from ax-c9 and other older axioms.

This proof uses newer axioms ax-4 and ax-6 , but since these are proved from the older axioms above, this is acceptable and lets us avoid having to reprove several earlier theorems to use ax-c4 and ax-c10 . (Contributed by NM, 21-Dec-2015) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	ax13fromc9	$$⊢\neg x=y\to \left(y=z\to \forall xy=z\right)$$

Proof

Step	Hyp	Ref	Expression
1		ax-c5	$$⊢\forall xx=y\to x=y$$
2	1	con3i	$$⊢\neg x=y\to \neg \forall xx=y$$
3		ax-c5	$$⊢\forall xx=z\to x=z$$
4	3	con3i	$$⊢\neg x=z\to \neg \forall xx=z$$
5		ax-c9	$$⊢\neg \forall xx=y\to \left(\neg \forall xx=z\to \left(y=z\to \forall xy=z\right)\right)$$
6	2 4 5	syl2im	$$⊢\neg x=y\to \left(\neg x=z\to \left(y=z\to \forall xy=z\right)\right)$$
7		ax13b	$$⊢\left(\neg x=y\to \left(y=z\to \forall xy=z\right)\right)\leftrightarrow \left(\neg x=y\to \left(\neg x=z\to \left(y=z\to \forall xy=z\right)\right)\right)$$
8	6 7	mpbir	$$⊢\neg x=y\to \left(y=z\to \forall xy=z\right)$$