This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nelaneqOLD

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	nelaneqOLD	$⊢ \neg (A \in B \land A = B)$

Proof

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