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) (Proof shortened by SN, 22-Apr-2026)

	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	2	biimparc	$$⊢\left(A\in B\wedge A=B\right)\to A\in A$$
4	1 3	mto	$$⊢\neg \left(A\in B\wedge A=B\right)$$