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 ) |
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 ) |