Metamath Proof Explorer


Theorem inton

Description: The intersection of the class of ordinal numbers is the empty set. (Contributed by NM, 20-Oct-2003)

Ref Expression
Assertion inton
|- |^| On = (/)

Proof

Step Hyp Ref Expression
1 0elon
 |-  (/) e. On
2 int0el
 |-  ( (/) e. On -> |^| On = (/) )
3 1 2 ax-mp
 |-  |^| On = (/)