proof shortened by theorems recently moved to main (#2830)
proof shortened by theorems recently moved to main (#2830)

* proofs shortened using ~exlimimdd

* proofs shortened using ~elvd

* proofs shortened using ~moimd

* proofs shortened using ~csbvargi

* proofs shortened using ~pwexd

* minimization of proof of ~rfovcnvf1od  redone
metamath/set.mm,metamath/set.mm,metamath/set.mm