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

---

Theorem sezni-elt 571

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 kei 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 kei sezni ko'a
3		df-sezni 570	. . . . . 6 ⊢ go pa ka ce'u bu'a ce'u ce'u kei sezni ko'a gi ge ko'a kloje pa ka ce'u bu'a ce'u ce'u kei 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 kei 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 466	. . 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 319   ce'u sc 340   pa spk 341   ro brdp 463   pa bpdp 555   kloje sbkloje 565   sezni sbsezni 569

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 465  df-sezni 570

This theorem is referenced by: (None)

Copyright terms: Public domain

W3C validator