Metamath Proof Explorer

Theorem neleq1

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

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

Proof

Step Hyp Ref Expression
1 id 
 |-  ( A = B -> A = B )
2 eqidd 
 |-  ( A = B -> C = C )
3 1 2 neleq12d 
 |-  ( A = B -> ( A e/ C <-> B e/ C ) )