Theorem dfom4

Description: A simplification of df-om assuming the Axiom of Infinity. (Contributed by NM, 30-May-2003)

	Ref	Expression
Assertion	dfom4	⊢ ω = { 𝑥 ∣ ∀ 𝑦 ( Lim 𝑦 → 𝑥 ∈ 𝑦 ) }

Proof

Step	Hyp	Ref	Expression
1		elom3	⊢ ( 𝑥 ∈ ω ↔ ∀ 𝑦 ( Lim 𝑦 → 𝑥 ∈ 𝑦 ) )
2	1	abbi2i	⊢ ω = { 𝑥 ∣ ∀ 𝑦 ( Lim 𝑦 → 𝑥 ∈ 𝑦 ) }