Theorem nelaneq

Description: A class is not an element of and equal to a class at the same time. Variant of elneq analogously to elnotel and en2lp . (Proposed by BJ, 18-Jun-2022.) (Contributed by AV, 18-Jun-2022) (Proof shortened by TM, 31-Dec-2025)

	Ref	Expression
Assertion	nelaneq	$$⊢\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)$$