Metamath Proof Explorer
Description: An element of an ordinal number equals the intersection with it.
(Contributed by NM, 11-Jun-1994)
|
|
Ref |
Expression |
|
Hypothesis |
on.1 |
|
|
Assertion |
onelini |
|
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
on.1 |
|
2 |
1
|
onelssi |
|
3 |
|
dfss |
|
4 |
2 3
|
sylib |
|