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

Metamath Proof Explorer

Theorem nordeq

Description: A member of an ordinal class is not equal to it. (Contributed by NM, 25-May-1998)

		Ref	Expression
	Assertion	nordeq	$⊢ (Ord A \land B \in A) \to A \neq B$

Step	Hyp	Ref	Expression
1		ordirr	$⊢ Ord A \to \neg A \in A$
2		eleq1	$⊢ A = B \to (A \in A \leftrightarrow B \in A)$
3	2	notbid	$⊢ A = B \to (\neg A \in A \leftrightarrow \neg B \in A)$
4	1 3	syl5ibcom	$⊢ Ord A \to (A = B \to \neg B \in A)$
5	4	necon2ad	$⊢ Ord A \to (B \in A \to A \neq B)$
6	5	imp	$⊢ (Ord A \land B \in A) \to A \neq B$