A convenience theorem particularly designed to remove dependencies on [ax-11] in conjunction with distinctors. (Contributed by Wolf Lammen, 2-Sep-2018.)
A convenience theorem particularly designed to remove dependencies on [ax-11] in conjunction with distinctors. (Contributed by Wolf Lammen, 2-Sep-2018.)