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)

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

Proof

Step	Hyp	Ref	Expression
1		elneq	$$⊢A\in B\to A\ne B$$
2		orc	$$⊢\neg A\in B\to \left(\neg A\in B\vee \neg A=B\right)$$
3		neneq	$$⊢A\ne B\to \neg A=B$$
4	3	olcd	$$⊢A\ne B\to \left(\neg A\in B\vee \neg A=B\right)$$
5	2 4	ja	$$⊢\left(A\in B\to A\ne B\right)\to \left(\neg A\in B\vee \neg A=B\right)$$
6	1 5	ax-mp	$$⊢\left(\neg A\in B\vee \neg A=B\right)$$
7		ianor	$$⊢\neg \left(A\in B\wedge A=B\right)\leftrightarrow \left(\neg A\in B\vee \neg A=B\right)$$
8	6 7	mpbir	$$⊢\neg \left(A\in B\wedge A=B\right)$$