Description: Two classes related by the indexed union of relation exponentiation
over the natural numbers (including zero) is equivalent to the
existence of at least one number such that the two classes are related
by that relationship power. (Contributed by RP, 2-Jun-2020)