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