Home brismu bridi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >   Home  >  Th. List  >  du-refl

Theorem du-refl 256
Description: {du} is reflexive. (Contributed by la korvo, 16-Aug-2023.) (Shortened by la korvo, 23-Jun-2024.)
Assertion
Ref Expression
du-reflko'a du ko'a

Proof of Theorem du-refl
Dummy variable bu'a is distinct from all other variables.
StepHypRef Expression
1 go-id 95 . 2go ko'a bu'a gi ko'a bu'a
21duris 255 1ko'a du ko'a
Colors of variables: sumti selbri bridi
This theorem was proved from axioms:  ax-mp 10  ax-k 11  ax-s 15  ax-ge-le 48  ax-ge-re 49  ax-ge-in 50  ax-gen2 227  ax-qi2 239
This theorem depends on definitions:  df-go 83  df-o 198  df-du 251
This theorem is referenced by:  du-sym-ganai  260  ceihi  268  ce-left  412  ce-right  413  subid  452  zilcmi-nomei  461  du-kinra  543
  Copyright terms: Public domain W3C validator