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

Metamath Proof Explorer

Theorem nelneq

Description: A way of showing two classes are not equal. (Contributed by NM, 1-Apr-1997)

		Ref	Expression
	Assertion	nelneq	$⊢ (A \in C \land \neg B \in C) \to \neg A = B$

Step	Hyp	Ref	Expression
1		eleq1	$⊢ A = B \to (A \in C \leftrightarrow B \in C)$
2	1	biimpcd	$⊢ A \in C \to (A = B \to B \in C)$
3	2	con3dimp	$⊢ (A \in C \land \neg B \in C) \to \neg A = B$