Description: Over the ordinal numbers, one may define the relation A _E B iff
A e. B and one finds that, under this ordering, On is a
well-ordered class, see epweon . This is a weak form of epelg which
only requires that we know B to be a set. (Contributed by RP, 27-Sep-2023)