![]() |
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 2014 | . . 3 ⊢ (𝑦 = 𝑥 → (𝑦 = 𝑥 → 𝑥 = 𝑥)) | |
2 | 1 | pm2.43i 52 | . 2 ⊢ (𝑦 = 𝑥 → 𝑥 = 𝑥) |
3 | ax6ev 1974 | . 2 ⊢ ∃𝑦 𝑦 = 𝑥 | |
4 | 2, 3 | exlimiiv 1935 | 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 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 |
This theorem depends on definitions: df-bi 206 df-ex 1783 |
This theorem is referenced by: nfequid 2017 equcomiv 2018 equcomi 2021 stdpc6 2032 equsb1v 2104 ax6dgen 2125 ax13dgen1 2134 ax13dgen3 2136 sbid 2248 exists1 2657 vjust 3476 dfv2 3478 vexOLD 3480 reu6 3720 sbc8g 3783 dfnul2 4323 dfnul2OLD 4325 dfnul3OLD 4326 dfnul4OLD 4327 ab0orv 4376 dfid3 5573 isso2i 5619 relop 5845 iotanul 6513 f1eqcocnv 7286 f1eqcocnvOLD 7287 poxp2 8116 mpoxopoveq 8191 frecseq123 8254 ttrclselem2 9708 dfac2b 10112 konigthlem 10550 hash2prde 14418 hashge2el2difr 14429 pospo 18285 mamulid 21912 mdetdiagid 22071 alexsubALTlem3 23522 trust 23703 isppw2 26586 xmstrkgc 28110 avril1 29683 sa-abvi 31661 wlimeq12 34722 bj-ssbid2 35444 bj-ssbid1 35446 mptsnunlem 36124 ax12eq 37717 elnev 43068 ipo0 43079 ifr0 43080 tratrb 43168 tratrbVD 43493 unirnmapsn 43784 hspmbl 45218 et-equeucl 45461 |
Copyright terms: Public domain | W3C validator |