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

Proof

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