feat(set_theory/zfc/basic): more trivial results (#18294)
This PR does multiple very simple things at once. Here's a rundown.
- Golf `Set.eq_empty`.
- Add `Set.eq_empty_or_nonempty`, `Set.insert_nonempty`, `Set.singleton_nonempty`, `Class.mem_def`, `Class.not_empty_hom`, `Class.univ_hom`, `Class.empty_Cong_to_Class`, `Class.empty_Class_to_Cong`.
- Tag `Class.mem_univ` as `simp`.
- Move `Set.to_set_sUnion` and `Set.sUnion_empty`, so that the theorems on singleton injectivity aren't interspersed with the union results.
