brismu bridi		< Previous   Next > Nearby theorems
Mirrors  >  Home  >   Home  >  Th. List  >  se-invo

---

Theorem se-invo 216

Description: {se} is an involution. (Contributed by la korvo, 18-Jul-2023.)

Hypothesis

Ref	Expression
se-invo.0	⊢ ko'a se se bu'a ko'e

Assertion

Ref	Expression
se-invo	⊢ ko'a bu'a ko'e

---

Proof of Theorem se-invo

Step	Hyp	Ref	Expression
1		se-invo.0	. . 3 ⊢ ko'a se se bu'a ko'e
2	1	sei 214	. 2 ⊢ ko'e se bu'a ko'a
3	2	sei 214	1 ⊢ ko'a bu'a ko'e

Colors of variables: sumti selbri bridi

Syntax hints:   se sbs 212

This theorem was proved from axioms:  ax-mp 10  ax-ge-le 48

This theorem depends on definitions:  df-go 83  df-se 213

This theorem is referenced by: (None)

Copyright terms: Public domain

W3C validator