brismu bridi		< Previous   Next > Nearby theorems
Mirrors  >  Home  >   Home  >  Th. List  >  sezni-elt

---

Theorem sezni-elt 468

Description: The identity element of monoids is unique. (Contributed by la korvo, 16-Oct-2024.)

Hypotheses

Ref	Expression
sezni-elt.0	⊢ 1 ka ce'u bu'a ce'u ce'u kei sezni ko'a
sezni-elt.1	⊢ da cmima ko'a

Assertion

Ref	Expression
sezni-elt	⊢ 1 de poi ke'a cmima ko'a ku'o zo'u ge da bu'a de da gi de bu'a da da

Distinct variable group:   da ,de

---

Proof of Theorem sezni-elt

Step	Hyp	Ref	Expression
1		sezni-elt.1	. 2 ⊢ da cmima ko'a
2		sezni-elt.0	. . . . . 6 ⊢ 1 ka ce'u bu'a ce'u ce'u kei sezni ko'a
3		df-sezni 467	. . . . . 6 ⊢ go 1 ka ce'u bu'a ce'u ce'u kei sezni ko'a gi ge ko'a kloje 1 ka ce'u bu'a ce'u ce'u kei gi ro da poi ke'a cmima ko'a ku'o zo'u 1 de poi ke'a cmima ko'a ku'o zo'u ge da bu'a de da gi de bu'a da da
4	2, 3	bi 69	. . . . 5 ⊢ ge ko'a kloje 1 ka ce'u bu'a ce'u ce'u kei gi ro da poi ke'a cmima ko'a ku'o zo'u 1 de poi ke'a cmima ko'a ku'o zo'u ge da bu'a de da gi de bu'a da da
5	4	ge-rei 39	. . . 4 ⊢ ro da poi ke'a cmima ko'a ku'o zo'u 1 de poi ke'a cmima ko'a ku'o zo'u ge da bu'a de da gi de bu'a da da
6	5	poi-roi 373	. . 3 ⊢ ro da zo'u ganai da cmima ko'a gi 1 de poi ke'a cmima ko'a ku'o zo'u ge da bu'a de da gi de bu'a da da
7	6	spec1i 182	. 2 ⊢ ganai da cmima ko'a gi 1 de poi ke'a cmima ko'a ku'o zo'u ge da bu'a de da gi de bu'a da da
8	1, 7	ax-mp 10	1 ⊢ 1 de poi ke'a cmima ko'a ku'o zo'u ge da bu'a de da gi de bu'a da da

Colors of variables: sumti selbri bridi

Syntax hints:  tsb 1  tss 2  ganai bgan 9  ge bge 33  ro brd 177  cmima sbcmima 246  ce'u sc 266  1 spk 267  ro brdp 370  1 bpd 454  1 bpdp 458  kloje sbkloje 464  sezni sbsezni 466

This theorem was proved from axioms:  ax-mp 10  ax-ge-le 34  ax-ge-re 35  ax-spec1 181

This theorem depends on definitions:  df-go 52  df-poi-ro 372  df-sezni 467

This theorem is referenced by: (None)

Copyright terms: Public domain

W3C validator