Theorem nelaneqOLD

Description: Obsolete version of nelaneq as of 22-Apr-2026. (Proposed by BJ, 18-Jun-2022.) (Contributed by AV, 18-Jun-2022) (Proof shortened by TM, 31-Dec-2025) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	nelaneqOLD	$$⊢\neg \left(A\in B\wedge A=B\right)$$

Proof

Step	Hyp	Ref	Expression
1		elirr	$$⊢\neg A\in A$$
2		eleq2	$$⊢A=B\to \left(A\in A\leftrightarrow A\in B\right)$$
3	1 2	mtbii	$$⊢A=B\to \neg A\in B$$
4	3	con2i	$$⊢A\in B\to \neg A=B$$
5		imnan	$$⊢\left(A\in B\to \neg A=B\right)\leftrightarrow \neg \left(A\in B\wedge A=B\right)$$
6	4 5	mpbi	$$⊢\neg \left(A\in B\wedge A=B\right)$$