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 ⊢∃x∈Onφ↔⋂x∈On|φ∈On

Proof

Step Hyp Ref Expression
1 intexrab ⊢∃x∈Onφ↔⋂x∈On|φ∈V
2 onintrab ⊢⋂x∈On|φ∈V↔⋂x∈On|φ∈On
3 1 2 bitri ⊢∃x∈Onφ↔⋂x∈On|φ∈On