Theorem ax13dgen2

Description: Degenerate instance of ax-13 where bundled variables x and z have a common substitution. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 13-Apr-2017)

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

Proof

Step	Hyp	Ref	Expression
1		equcomi	$$⊢y=x\to x=y$$
2		pm2.21	$$⊢\neg x=y\to \left(x=y\to \forall xy=x\right)$$
3	1 2	syl5	$$⊢\neg x=y\to \left(y=x\to \forall xy=x\right)$$