Metamath Proof Explorer

Theorem neleq2

Description: Equality theorem for negated membership. (Contributed by NM, 20-Nov-1994) (Proof shortened by Wolf Lammen, 25-Nov-2019)

Ref Expression
Assertion neleq2 
|- ( A = B -> ( C e/ A <-> C e/ B ) )

Proof

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 ) )