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

Metamath Proof Explorer

Theorem dfom4

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

		Ref	Expression
	Assertion	dfom4	$⊢ ω = \{x \| \forall y (Lim y \to x \in y)\}$

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