Description: The intersection of the class of ordinal numbers is the empty set. (Contributed by NM, 20-Oct-2003)
Ref | Expression | ||
---|---|---|---|
Assertion | inton | |- |^| On = (/) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 0elon | |- (/) e. On |
|
2 | int0el | |- ( (/) e. On -> |^| On = (/) ) |
|
3 | 1 2 | ax-mp | |- |^| On = (/) |