Description: If x is disjoint from A , then x is not free in A . (Contributed by Mario Carneiro, 7Oct2016)
Ref  Expression  

Assertion  nfcvd   ( ph > F/_ x A ) 
Step  Hyp  Ref  Expression 

1  nfcv   F/_ x A 

2  1  a1i   ( ph > F/_ x A ) 