Metamath Proof Explorer


Theorem equid1ALT

Description: Alternate proof of equid and equid1 from older axioms ax-c7 , ax-c10 and ax-c9 . (Contributed by NM, 10-Jan-1993) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion equid1ALT x=x

Proof

Step Hyp Ref Expression
1 ax-c9 ¬xx=x¬xx=xx=xxx=x
2 1 pm2.43i ¬xx=xx=xxx=x
3 2 alimi x¬xx=xxx=xxx=x
4 ax-c10 xx=xxx=xx=x
5 3 4 syl x¬xx=xx=x
6 ax-c7 ¬x¬xx=xx=x
7 5 6 pm2.61i x=x