Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > equid | Structured version Visualization version GIF version |
Description: Identity law for equality. Lemma 2 of [KalishMontague] p. 85. See also Lemma 6 of [Tarski] p. 68. (Contributed by NM, 1-Apr-2005.) (Revised by NM, 9-Apr-2017.) (Proof shortened by Wolf Lammen, 22-Aug-2020.) |
Ref | Expression |
---|---|
equid | ⊢ 𝑥 = 𝑥 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax7v1 2008 | . . 3 ⊢ (𝑦 = 𝑥 → (𝑦 = 𝑥 → 𝑥 = 𝑥)) | |
2 | 1 | pm2.43i 52 | . 2 ⊢ (𝑦 = 𝑥 → 𝑥 = 𝑥) |
3 | ax6ev 1963 | . 2 ⊢ ∃𝑦 𝑦 = 𝑥 | |
4 | 2, 3 | exlimiiv 1923 | 1 ⊢ 𝑥 = 𝑥 |
Colors of variables: wff setvar class |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 |
This theorem depends on definitions: df-bi 208 df-ex 1772 |
This theorem is referenced by: nfequid 2011 equcomiv 2012 equcomi 2015 stdpc6 2026 equsb1v 2103 ax6dgen 2123 ax13dgen1 2132 ax13dgen3 2134 sbid 2247 exists1 2741 vjust 3493 vex 3495 vexOLD 3496 reu6 3714 sbc8g 3777 dfnul2 4290 dfnul3 4292 dfid3 5455 isso2i 5501 relop 5714 domepOLD 5787 iotanul 6326 f1eqcocnv 7048 fsplitOLD 7802 mpoxopoveq 7874 ruv 9054 dfac2b 9544 konigthlem 9978 hash2prde 13816 hashge2el2difr 13827 pospo 17571 mamulid 20978 mdetdiagid 21137 alexsubALTlem3 22585 trust 22765 isppw2 25619 xmstrkgc 26599 avril1 28169 sa-abvi 30147 wlimeq12 33003 frecseq123 33016 bj-ssbid2 33892 bj-ssbid1 33894 mptsnunlem 34501 ax12eq 35957 elnev 40647 ipo0 40658 ifr0 40659 tratrb 40747 tratrbVD 41072 unirnmapsn 41353 hspmbl 42788 |
Copyright terms: Public domain | W3C validator |