Description: Bound-variable hypothesis builder for indexed union. Usage of this
theorem is discouraged because it depends on ax-13 , see nfiund for
a weaker version that does not require it. (Contributed by Emmett
Weisz, 6-Dec-2019)(New usage is discouraged.)