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 )