Description: Alternate proof of exel , avoiding ax-pr but requiring ax-5 ,
ax-9 , and ax-pow . This is similar to how elALT2 uses ax-pow instead of ax-pr compared to el . (Contributed by SN, 18-Sep-2023)(Proof modification is discouraged.)(New usage is discouraged.)