Theorem ax13ALT

Description: Alternate proof of ax13 from FOL, sp , and axc9 . (Contributed by NM, 21-Dec-2015) (Proof shortened by Wolf Lammen, 31-Jan-2018) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		sp	$$⊢\forall xx=y\to x=y$$
2	1	con3i	$$⊢\neg x=y\to \neg \forall xx=y$$
3		sp	$$⊢\forall xx=z\to x=z$$
4	3	con3i	$$⊢\neg x=z\to \neg \forall xx=z$$
5		axc9	$$⊢\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)$$