Description: Boundvariable hypothesis builder for inequality. (Contributed by NM, 10Nov2007) (Revised by Mario Carneiro, 7Oct2016)
Ref  Expression  

Hypotheses  nfne.1   F/_ x A 

nfne.2   F/_ x B 

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

1  nfne.1   F/_ x A 

2  nfne.2   F/_ x B 

3  dfne   ( A =/= B <> . A = B ) 

4  1 2  nfeq   F/ x A = B 
5  4  nfn   F/ x . A = B 
6  3 5  nfxfr   F/ x A =/= B 