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

Metamath Proof Explorer

Theorem onsssuc

Description: A subset of an ordinal number belongs to its successor. (Contributed by NM, 15-Sep-1995)

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

Step	Hyp	Ref	Expression
1		eloni	$⊢ B \in On \to Ord B$
2		ordsssuc	$⊢ (A \in On \land Ord B) \to (A \subseteq B \leftrightarrow A \in suc B)$
3	1 2	sylan2	$⊢ (A \in On \land B \in On) \to (A \subseteq B \leftrightarrow A \in suc B)$