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 
|- _om = { x | A. y ( Lim y -> x e. y ) }

Proof

Step Hyp Ref Expression
1 elom3 
 |-  ( x e. _om <-> A. y ( Lim y -> x e. y ) )
2 1 eqabi 
 |-  _om = { x | A. y ( Lim y -> x e. y ) }