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


Ref 
Expression 

Assertion 
neleq1 
$${\u22a2}{A}={B}\to \left({A}\notin {C}\leftrightarrow {B}\notin {C}\right)$$ 
Proof
Step 
Hyp 
Ref 
Expression 
1 

id 
$${\u22a2}{A}={B}\to {A}={B}$$ 
2 

eqidd 
$${\u22a2}{A}={B}\to {C}={C}$$ 
3 
1 2

neleq12d 
$${\u22a2}{A}={B}\to \left({A}\notin {C}\leftrightarrow {B}\notin {C}\right)$$ 