Metamath Proof Explorer

Theorem onelpss

Description: Relationship between membership and proper subset of an ordinal number. (Contributed by NM, 15-Sep-1995)

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

Step	Hyp	Ref	Expression
1		eloni	$⊢ A \in On \to Ord A$
2		eloni	$⊢ B \in On \to Ord B$
3		ordelssne	$⊢ (Ord A \land Ord B) \to (A \in B \leftrightarrow (A \subseteq B \land A \neq B))$
4	1 2 3	syl2an	$⊢ (A \in On \land B \in On) \to (A \in B \leftrightarrow (A \subseteq B \land A \neq B))$