Description: Boundvariable hypothesis builder for substitution into a class. (Contributed by NM, 17Aug2006) (Revised by Mario Carneiro, 12Oct2016)
Ref  Expression  

Assertion  nfcsb1v   F/_ x [_ A / x ]_ B 
Step  Hyp  Ref  Expression 

1  nfcv   F/_ x A 

2  1  nfcsb1   F/_ x [_ A / x ]_ B 