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

Hypotheses  nfned.1   ( ph > F/_ x A ) 

nfned.2   ( ph > F/_ x B ) 

Assertion  nfned   ( ph > F/ x A =/= B ) 
Step  Hyp  Ref  Expression 

1  nfned.1   ( ph > F/_ x A ) 

2  nfned.2   ( ph > F/_ x B ) 

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

4  1 2  nfeqd   ( ph > F/ x A = B ) 
5  4  nfnd   ( ph > F/ x . A = B ) 
6  3 5  nfxfrd   ( ph > F/ x A =/= B ) 