Theorem dfom4

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

	Ref	Expression
Assertion	dfom4	$$⊢\mathrm{\omega }=\left\{x|\forall y\left(\mathrm{Lim}y\to x\in y\right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		elom3	$$⊢x\in \mathrm{\omega }\leftrightarrow \forall y\left(\mathrm{Lim}y\to x\in y\right)$$
2	1	eqabi	$$⊢\mathrm{\omega }=\left\{x|\forall y\left(\mathrm{Lim}y\to x\in y\right)\right\}$$