mathlib3

996b0ff9 - feat(set_theory/zfc/basic): more basic simp/ext lemmas (#18233)

feat(set_theory/zfc/basic): more basic simp/ext lemmas (#18233) We prove class extensionality, the characterization of class unions, and other very simple results.