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