| 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 2009 | . . 3 ⊢ (𝑦 = 𝑥 → (𝑦 = 𝑥 → 𝑥 = 𝑥)) | |
| 2 | 1 | pm2.43i 52 | . 2 ⊢ (𝑦 = 𝑥 → 𝑥 = 𝑥) |
| 3 | ax6ev 1969 | . 2 ⊢ ∃𝑦 𝑦 = 𝑥 | |
| 4 | 2, 3 | exlimiiv 1931 | 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 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 |
| This theorem depends on definitions: df-bi 207 df-ex 1780 |
| This theorem is referenced by: nfequid 2012 equcomiv 2013 equcomi 2016 stdpc6 2027 equsb1v 2105 ax6dgen 2128 ax13dgen1 2137 ax13dgen3 2139 sbid 2255 exists1 2660 vjust 3480 dfv2 3482 reu6 3731 sbc8g 3795 dfnul2 4335 ab0orv 4382 dfid3 5579 isso2i 5627 relop 5859 iotanul 6537 f1eqcocnv 7319 poxp2 8164 mpoxopoveq 8240 frecseq123 8303 ttrclselem2 9762 dfac2b 10167 konigthlem 10604 hash2prde 14505 hashge2el2difr 14516 pospo 18386 mamulid 22437 mdetdiagid 22596 alexsubALTlem3 24047 trust 24228 isppw2 27148 xmstrkgc 28890 avril1 30472 sa-abvi 32452 wlimeq12 35798 bj-ssbid2 36641 bj-ssbid1 36643 mptsnunlem 37317 ax12eq 38920 elnev 44435 ipo0 44446 ifr0 44447 tratrb 44534 tratrbVD 44859 unirnmapsn 45192 hspmbl 46617 et-equeucl 46860 |
| Copyright terms: Public domain | W3C validator |