Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > equid | Structured version Visualization version Unicode 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, 5-Feb-2018.) (Proof shortened by Wolf Lammen, 22-Aug-2020.) |
Ref | Expression |
---|---|
equid |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax7v1 1937 | . . 3 | |
2 | 1 | pm2.43i 52 | . 2 |
3 | ax6ev 1890 | . 2 | |
4 | 2, 3 | exlimiiv 1859 | 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 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 |
This theorem depends on definitions: df-bi 197 df-ex 1705 |
This theorem is referenced by: nfequid 1940 equcomiv 1941 equcomi 1944 stdpc6 1957 ax6dgen 2005 ax13dgen1 2014 ax13dgen3 2016 sbid 2114 exists1 2561 vjust 3201 vex 3203 reu6 3395 nfccdeq 3433 sbc8g 3443 dfnul3 3918 rab0OLD 3956 int0OLD 4491 dfid3 5025 isso2i 5067 relop 5272 iotanul 5866 f1eqcocnv 6556 fsplit 7282 mpt2xopoveq 7345 ruv 8507 dfac2 8953 konigthlem 9390 hash2prde 13252 hashge2el2difr 13263 pospo 16973 mamulid 20247 mdetdiagid 20406 alexsubALTlem3 21853 trust 22033 isppw2 24841 xmstrkgc 25766 avril1 27319 foo3 29302 domep 31698 wlimeq12 31765 bj-ssbid2 32645 bj-ssbid1 32647 bj-vjust 32786 mptsnunlem 33185 ax12eq 34226 elnev 38639 ipo0 38653 ifr0 38654 tratrb 38746 tratrbVD 39097 unirnmapsn 39406 hspmbl 40843 |
Copyright terms: Public domain | W3C validator |