Description: If x is not free in ph , it is not free in A. y ph . (Contributed by Mario Carneiro, 11Aug2016)
Ref  Expression  

Hypothesis  nfal.1   F/ x ph 

Assertion  nfal   F/ x A. y ph 
Step  Hyp  Ref  Expression 

1  nfal.1   F/ x ph 

2  1  nf5ri   ( ph > A. x ph ) 
3  2  hbal   ( A. y ph > A. x A. y ph ) 
4  3  nf5i   F/ x A. y ph 