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 = (/)