Metamath Proof Explorer

Table of Contents - 5.8.5. Reflexive-transitive closure as an indexed union

  1. crtrcl
  2. df-rtrclrec
  3. rtrclreclem1
  4. dfrtrclrec2
  5. rtrclreclem2
  6. rtrclreclem3
  7. rtrclreclem4
  8. dfrtrcl2