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 On
Assertion onelini B A B = B A

Proof

Step Hyp Ref Expression
1 on.1 A On
2 1 onelssi B A B A
3 dfss B A B = B A
4 2 3 sylib B A B = B A