Description: Bound-variable hypothesis builder for a class abstraction. Usage of
this theorem is discouraged because it depends on ax-13 . Use the
weaker nfabdw when possible. (Contributed by Mario Carneiro, 8-Oct-2016) Avoid ax-9 and ax-ext . (Revised by Wolf Lammen, 23-May-2023)(New usage is discouraged.)