brismu bridi		< Previous   Next > Nearby theorems
Mirrors  >  Home  >   Home  >  Th. List  >  id

---

Theorem id 16

Description: The principle of identity. This is distantly related to, but not the same as, the identity relation df-du 167. In terms of category theory, this proves that identity arrows exist. (Contributed by la korvo, 27-Jul-2023.)

Assertion

Ref	Expression
id	⊢ ganai broda gi broda

---

Proof of Theorem id

Step	Hyp	Ref	Expression
1		ax-k 10	. 2 ⊢ ganai broda gi ganai brode gi broda
2		ax-k 10	. 2 ⊢ ganai broda gi ganai ganai brode gi broda gi broda
3	1, 2	mpd 15	1 ⊢ ganai broda gi broda

Colors of variables: sumti selbri bridi

Syntax hints:  ganai bgan 8

This theorem was proved from axioms:  ax-mp 9  ax-k 10  ax-s 13

This theorem is referenced by:  ganai-swap12  25  ganai-abs  28  mpancom  45  go-refl  60  ga-lin  119  ga-rin  120  na-gaiho  188

Copyright terms: Public domain

W3C validator