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

Hypothesis  nfeq1.1   F/_ x A 

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

1  nfeq1.1   F/_ x A 

2  nfcv   F/_ x B 

3  1 2  nfeq   F/ x A = B 