Description: Two classes related by the indexed union of relation exponentiation
over the natural numbers 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)