Description: Bound-variable hypothesis builder for substitution into a class. Version of nfcsb with a disjoint variable condition, which does not require ax-13 . (Contributed by Mario Carneiro, 12-Oct-2016) Avoid ax-13 . (Revised by GG, 10-Jan-2024)
|- F/_ x A
|- F/_ x B
|- F/_ x [_ A / y ]_ B
|- [_ A / y ]_ B = { z | [. A / y ]. z e. B }
|- F/ z T.
|- F/ y T.
|- ( T. -> F/_ x A )
|- ( T. -> F/_ x B )
|- ( T. -> F/ x z e. B )
|- ( T. -> F/ x [. A / y ]. z e. B )
|- ( T. -> F/_ x { z | [. A / y ]. z e. B } )
|- ( T. -> F/_ x [_ A / y ]_ B )