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\to \left(C\notin A\leftrightarrow C\notin B\right)$$

Proof

Step	Hyp	Ref	Expression
1		eqidd	$$⊢A=B\to C=C$$
2		id	$$⊢A=B\to A=B$$
3	1 2	neleq12d	$$⊢A=B\to \left(C\notin A\leftrightarrow C\notin B\right)$$