Theorem eqid

Description: Law of identity (reflexivity of class equality). Theorem 6.4 of Quine p. 41.

This is part of Frege's eighth axiom per Proposition 54 of Frege1879 p. 50; see also biid . An early mention of this law can be found in Aristotle,Metaphysics, Z.17, 1041a10-20. (Thanks to Stefan Allan and BJ for this information.) (Contributed by NM, 21-Jun-1993) (Revised by BJ, 14-Oct-2017)

	Ref	Expression
Assertion	eqid	$$⊢A=A$$

Proof

Step	Hyp	Ref	Expression
1		biid	$$⊢x\in A\leftrightarrow x\in A$$
2	1	eqriv	$$⊢A=A$$