Theorem eqid1

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

This law is thought to have originated with Aristotle (_Metaphysics_, Book VII, Part 17). It is one of the three axioms of Ayn Rand's philosophy (_Atlas Shrugged_, Part Three, Chapter VII). While some have proposed extending Rand's axiomatization to include Compassion and Kindness, others fear that such an extension may flirt with logical inconsistency. (Contributed by Stefan Allan, 1-Apr-2009) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	eqid1	⊢ 𝐴 = 𝐴

Proof

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