mathlib3

f05fdcac - refactor(set_theory/zfc): make `Class` morally `Set → Prop` (#15248)

refactor(set_theory/zfc): make `Class` morally `Set → Prop` (#15248) We use `Class` in place of `Set → Prop` (within the `Class` API), and document this decision. Note that there's no longer much reason to have `Class.to_Set` separately from `Class.mem`. I will suggest inlining both into the `has_mem` instance in a followup PR. See [Zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/ZFC.20definable.20class/near/289194801)).