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

Metamath Proof Explorer

Theorem onelini

Description: An element of an ordinal number equals the intersection with it. (Contributed by NM, 11-Jun-1994)

		Ref	Expression
	Hypothesis	on.1	$⊢ A \in On$
	Assertion	onelini	$⊢ B \in A \to B = B \cap A$

Step	Hyp	Ref	Expression
1		on.1	$⊢ A \in On$
2	1	onelssi	$⊢ B \in A \to B \subseteq A$
3		dfss	$⊢ B \subseteq A \leftrightarrow B = B \cap A$
4	2 3	sylib	$⊢ B \in A \to B = B \cap A$