Metamath Proof Explorer

Theorem onsseleq

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

		Ref	Expression
	Assertion	onsseleq	$⊢ (A \in On \land B \in On) \to (A \subseteq B \leftrightarrow (A \in B \lor A = B))$

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