Theorem equidqe

Description: equid with existential quantifier without using ax-c5 or ax-5 . (Contributed by NM, 13-Jan-2011) (Proof shortened by Wolf Lammen, 27-Feb-2014) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	equidqe	$$⊢\neg \forall y\neg x=x$$

Proof

Step	Hyp	Ref	Expression
1		ax6fromc10	$$⊢\neg \forall y\neg y=x$$
2		ax7	$$⊢y=x\to \left(y=x\to x=x\right)$$
3	2	pm2.43i	$$⊢y=x\to x=x$$
4	3	con3i	$$⊢\neg x=x\to \neg y=x$$
5	4	alimi	$$⊢\forall y\neg x=x\to \forall y\neg y=x$$
6	1 5	mto	$$⊢\neg \forall y\neg x=x$$