# Metamath Proof Explorer

## Theorem elom

Description: Membership in omega. The left conjunct can be eliminated if we assume the Axiom of Infinity; see elom3 . (Contributed by NM, 15-May-1994)

Ref Expression
Assertion elom ${⊢}{A}\in \mathrm{\omega }↔\left({A}\in \mathrm{On}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\left(\mathrm{Lim}{x}\to {A}\in {x}\right)\right)$

### Proof

Step Hyp Ref Expression
1 eleq1 ${⊢}{y}={A}\to \left({y}\in {x}↔{A}\in {x}\right)$
2 1 imbi2d ${⊢}{y}={A}\to \left(\left(\mathrm{Lim}{x}\to {y}\in {x}\right)↔\left(\mathrm{Lim}{x}\to {A}\in {x}\right)\right)$
3 2 albidv ${⊢}{y}={A}\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}\left(\mathrm{Lim}{x}\to {y}\in {x}\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\left(\mathrm{Lim}{x}\to {A}\in {x}\right)\right)$
4 df-om ${⊢}\mathrm{\omega }=\left\{{y}\in \mathrm{On}|\forall {x}\phantom{\rule{.4em}{0ex}}\left(\mathrm{Lim}{x}\to {y}\in {x}\right)\right\}$
5 3 4 elrab2 ${⊢}{A}\in \mathrm{\omega }↔\left({A}\in \mathrm{On}\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\left(\mathrm{Lim}{x}\to {A}\in {x}\right)\right)$