Metamath Proof Explorer


Theorem onintrab

Description: The intersection of a class of ordinal numbers exists iff it is an ordinal number. (Contributed by NM, 6-Nov-2003)

Ref Expression
Assertion onintrab xOn|φVxOn|φOn

Proof

Step Hyp Ref Expression
1 intex xOn|φxOn|φV
2 ssrab2 xOn|φOn
3 oninton xOn|φOnxOn|φxOn|φOn
4 2 3 mpan xOn|φxOn|φOn
5 1 4 sylbir xOn|φVxOn|φOn
6 elex xOn|φOnxOn|φV
7 5 6 impbii xOn|φVxOn|φOn