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

---

Theorem sezni-elt 577

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

Hypotheses

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

Assertion

Ref	Expression
sezni-elt	⊢ pa 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 ⊢ pa ka ce'u bu'a ce'u ce'u ku sezni ko'a
3		df-sezni 576	. . . . . 6 ⊢ go pa ka ce'u bu'a ce'u ce'u ku sezni ko'a gi ge ko'a kloje pa ka ce'u bu'a ce'u ce'u ku gi ro da poi ke'a cmima ko'a ku'o zo'u pa 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 101	. . . . 5 ⊢ ge ko'a kloje pa ka ce'u bu'a ce'u ce'u ku gi ro da poi ke'a cmima ko'a ku'o zo'u pa 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 53	. . . 4 ⊢ ro da poi ke'a cmima ko'a ku'o zo'u pa 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 472	. . 3 ⊢ ro da zo'u ganai da cmima ko'a gi pa 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 229	. 2 ⊢ ganai da cmima ko'a gi pa 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 ⊢ pa 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 47   cmima sbcmima 320   ce'u sc 341   pa spk 342   ro brdp 469   pa bpdp 561   kloje sbkloje 571   sezni sbsezni 575

This theorem was proved from axioms:  ax-mp 10  ax-ge-le 48  ax-ge-re 49  ax-spec1 228

This theorem depends on definitions:  df-go 83  df-poi-ro 471  df-sezni 576

This theorem is referenced by: (None)

Copyright terms: Public domain

W3C validator