Metamath Proof Explorer


Theorem onintrab2

Description: An existence condition equivalent to an intersection's being an ordinal number. (Contributed by NM, 6-Nov-2003)

Ref Expression
Assertion onintrab2
|- ( E. x e. On ph <-> |^| { x e. On | ph } e. On )

Proof

Step Hyp Ref Expression
1 intexrab
 |-  ( E. x e. On ph <-> |^| { x e. On | ph } e. _V )
2 onintrab
 |-  ( |^| { x e. On | ph } e. _V <-> |^| { x e. On | ph } e. On )
3 1 2 bitri
 |-  ( E. x e. On ph <-> |^| { x e. On | ph } e. On )