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

---

Theorem sezni-elt 510

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 509	. . . . . 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 79	. . . . 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 48	. . . 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 415	. . 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 197	. 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 42  ro brd 191  cmima sbcmima 282  ce'u sc 303  1 spk 304  ro brdp 412  1 bpd 496  1 bpdp 500  kloje sbkloje 506  sezni sbsezni 508

This theorem was proved from axioms:  ax-mp 10  ax-ge-le 43  ax-ge-re 44  ax-spec1 196

This theorem depends on definitions:  df-go 61  df-poi-ro 414  df-sezni 509

This theorem is referenced by: (None)

Copyright terms: Public domain

W3C validator