![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > eqid1 | Structured version Visualization version GIF version |
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 |
---|---|
eqid1 | ⊢ 𝐴 = 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | biid 264 | . 2 ⊢ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴) | |
2 | 1 | eqriv 2795 | 1 ⊢ 𝐴 = 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1538 ∈ wcel 2111 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-9 2121 ax-ext 2770 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1782 df-cleq 2791 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |