Description: Hypothesis builder for equality, special case. (Contributed by Mario Carneiro, 10Oct2016)
Ref  Expression  

Hypothesis  nfeq2.1   F/_ x B 

Assertion  nfeq2   F/ x A = B 
Step  Hyp  Ref  Expression 

1  nfeq2.1   F/_ x B 

2  nfcv   F/_ x A 

3  2 1  nfeq   F/ x A = B 