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

Proof

Step Hyp Ref Expression
1 intex ⊢ x ∈ On | φ ≠ ∅ ↔ ⋂ x ∈ On | φ ∈ V
2 ssrab2 ⊢ x ∈ On | φ ⊆ On
3 oninton ⊢ x ∈ On | φ ⊆ On ∧ x ∈ On | φ ≠ ∅ → ⋂ x ∈ On | φ ∈ On
4 2 3 mpan ⊢ x ∈ On | φ ≠ ∅ → ⋂ x ∈ On | φ ∈ On
5 1 4 sylbir ⊢ ⋂ x ∈ On | φ ∈ V → ⋂ x ∈ On | φ ∈ On
6 elex ⊢ ⋂ x ∈ On | φ ∈ On → ⋂ x ∈ On | φ ∈ V
7 5 6 impbii ⊢ ⋂ x ∈ On | φ ∈ V ↔ ⋂ x ∈ On | φ ∈ On