Metamath Proof Explorer


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