Description: Bound-variable hypothesis builder for class substitution. Usage of this
theorem is discouraged because it depends on ax-13 . Use the weaker
nfsbcw when possible. (Contributed by NM, 7-Sep-2014)(Revised by Mario Carneiro, 12-Oct-2016)(New usage is discouraged.)