Theorem nelaneqOLDOLD

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

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