This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ∃ 𝑥 ∈ On 𝜑 ↔ ∩ { 𝑥 ∈ On ∣ 𝜑 } ∈ On )

Proof

Step Hyp Ref Expression
1 intexrab ⊢ ( ∃ 𝑥 ∈ On 𝜑 ↔ ∩ { 𝑥 ∈ On ∣ 𝜑 } ∈ V )
2 onintrab ⊢ ( ∩ { 𝑥 ∈ On ∣ 𝜑 } ∈ V ↔ ∩ { 𝑥 ∈ On ∣ 𝜑 } ∈ On )
3 1 2 bitri ⊢ ( ∃ 𝑥 ∈ On 𝜑 ↔ ∩ { 𝑥 ∈ On ∣ 𝜑 } ∈ On )