id - brismu bridi

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

Theorem id 19

Description: The principle of identity. This is distantly related to, but not the same as, the identity relation df-du 251. 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 11	. 2 ⊢ ganai broda gi ganai brode gi broda
2		ax-k 11	. 2 ⊢ ganai broda gi ganai ganai brode gi broda gi broda
3	1, 2	mpd 18	1 ⊢ ganai broda gi broda

Colors of variables: sumti selbri bridi

Syntax hints: ganai bgan 9

This theorem was proved from axioms: ax-mp 10 ax-k 11 ax-s 15

This theorem is referenced by: idd 20 ganai-swap12 29 mpc 31 ganai-abs 34 ganai-comp-rl 39 ganai-comp-lr 46 mpancom 71 mpdan 72 ge-pair 79 ge-pairl 80 ge-pairr 81 go-id 95 na.a-refl 114 ga-lin 165 ga-rin 166 ga-idem 171 ga-pairl 180 ga-pairr 181 na-gaiho 280 con2i 292 nakunaku 293 wit 423 foml19.41 432 nibli-refl 510 kihirnihi-refl 679

W3C validator