extend df-relexp to be compatible with df-trcl
extend df-relexp to be compatible with df-trcl

rebuild all theorems that used to depend on df-relexp to depend on df-relexpNEW

* relexp0 -> relexp0d
* relexp1 -> relexp1d (one less hypothesis)
* relexpsucr -> relexpsucrd
* relexpsucl -> relexpsucld
* relexpcnv -> relexpcnvd (one less hypothesis)
* relexprel -> relexpreld
* relexpdm -> relexpdmd (one less hypothesis)
* relexprn -> relexprnd (one less hypothesis)
* relexpfld -> relexpfldd (one less hypothesis)
* relexpadd -> relexpaddd
* relexpindlem -> relexpindlemNEW
* relexpind -> relexpindNEW
* rtrclreclem.subset -> rtrclreclem.subsetNEW (one less hypothesis)
* rtrclreclem.refl -> rtrclreclem.reflNEW
* rtrclreclem.trans -> rtrclreclem.transNEW
* rtrclreclem.min -> rtrclreclem.minNEW
* dfrtrcl2 -> dfrtrcl2NEW
* rtrclind -> rtrclindNEW

Additional lemmas and theorems leveraging df-relexpNEW (mostly in closed form)

* relexp0g
* relexp0NEW
* relexp1g
* relexpsucnnr
* relexpsucnnl
* relexpsucrNEW
* relexpsuclNEW
* relexpcnvNEW
* relexp0rel
* relexprelg
* relexprelNEW
* relexpuzrel
* relexpnndm
* relexpdmg
* relexpdmNEW
* relexpnnrn
* relexprng
* relexprnNEW
* relexpfldNEW
* relexpaddnn
* relexpaddg

New lemmas and theorems on the transitive closure of a relation

* cleq1lem
* cleq1
* trcleq1
* clsslem
* trclsslem
* trcleq2lem
* cvbtrcl
* trcleq12lem
* trclexlem
* trclublem
* trclubi
* trclubgi

* trclfv
* brtrclfv
* brcnvtrclfv
* brtrclfvcnv
* brcnvtrclfvcnv
* trclfvss
* trclfvub
* trclfvlb
* trclfvcotr
* trclfvlb2
* trclfvlb3
* cotrtrclfv
* trclidm
* trclun
* trclfvg
* trclfvcotrg
* reltrclfv
* cnvtrclfv
* dmtrclfv
* lem1frege76a
* lem2frege76a

Work in progress

* trclubgres
* brcnvtrclfv2
* rntrclfv
* trclfvres
* trclfvdecom
* trclfvimadecom
* trclfvresub
* trclimaub
* trclunxp
* dffrege76

metamath/set.mm,metamath/set.mm,metamath/set.mm