Description: Boundvariable hypothesis builder for restricted quantification. Version of nfral with a disjoint variable condition, which does not require ax13 . (Contributed by NM, 1Sep1999) (Revised by Gino Giotto, 10Jan2024)
Ref  Expression  

Hypotheses  nfralw.1   F/_ x A 

nfralw.2   F/ x ph 

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

1  nfralw.1   F/_ x A 

2  nfralw.2   F/ x ph 

3  nftru   F/ y T. 

4  1  a1i   ( T. > F/_ x A ) 
5  2  a1i   ( T. > F/ x ph ) 
6  3 4 5  nfraldw   ( T. > F/ x A. y e. A ph ) 
7  6  mptru   F/ x A. y e. A ph 