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 𝐴 = 𝐴


Step Hyp Ref Expression
1 biid ( 𝑥𝐴𝑥𝐴 )
2 1 eqriv 𝐴 = 𝐴