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

Metamath Proof Explorer

Theorem ordelssne

Description: For ordinal classes, membership is equivalent to strict inclusion. Corollary 7.8 of TakeutiZaring p. 37. (Contributed by NM, 25-Nov-1995)

		Ref	Expression
	Assertion	ordelssne	$⊢ (Ord A \land Ord B) \to (A \in B \leftrightarrow (A \subseteq B \land A \neq B))$

Proof

Step	Hyp	Ref	Expression
1		ordtr	$⊢ Ord A \to Tr A$
2		tz7.7	$⊢ (Ord B \land Tr A) \to (A \in B \leftrightarrow (A \subseteq B \land A \neq B))$
3	1 2	sylan2	$⊢ (Ord B \land Ord A) \to (A \in B \leftrightarrow (A \subseteq B \land A \neq B))$
4	3	ancoms	$⊢ (Ord A \land Ord B) \to (A \in B \leftrightarrow (A \subseteq B \land A \neq B))$