Commit 2020-10-16 07:43 f675a006

chore(set_theory/zfc): split long lines (#4641) Also add Set.subset_def and rewrite Set.mem_pair_sep in tactic mode

modified theorem Class.sep_hom

modified theorem Set.image.mk

modified theorem Set.map_fval

modified theorem Set.map_is_func

modified theorem Set.map_unique

modified theorem Set.mem_image

modified theorem Set.mem_map

modified theorem Set.mem_pair_sep

added theorem Set.subset_def

modified theorem pSet.definable.eq