Theorem equidq

Description: equid with universal quantifier without using ax-c5 or ax-5 . (Contributed by NM, 13-Jan-2011) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	equidq	$$⊢\forall yx=x$$

Proof

Step	Hyp	Ref	Expression
1		equidqe	$$⊢\neg \forall y\neg x=x$$
2		ax10fromc7	$$⊢\neg \forall yx=x\to \forall y\neg \forall yx=x$$
3		hbequid	$$⊢x=x\to \forall yx=x$$
4	3	con3i	$$⊢\neg \forall yx=x\to \neg x=x$$
5	2 4	alrimih	$$⊢\neg \forall yx=x\to \forall y\neg x=x$$
6	1 5	mt3	$$⊢\forall yx=x$$