Description: Equality theorem for negated membership. (Contributed by NM, 20Nov1994) (Proof shortened by Wolf Lammen, 25Nov2019)
Ref  Expression  

Assertion  neleq2   ( A = B > ( C e/ A <> C e/ B ) ) 
Step  Hyp  Ref  Expression 

1  eqidd   ( A = B > C = C ) 

2  id   ( A = B > A = B ) 

3  1 2  neleq12d   ( A = B > ( C e/ A <> C e/ B ) ) 