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 e. A <-> x e. A )
2	1	eqriv	|- A = A