Theorem elom3

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

	Ref	Expression
Assertion	elom3	|- ( A e. _om <-> A. x ( Lim x -> A e. x ) )

Proof

Step	Hyp	Ref	Expression
1		elom	|- ( A e. _om <-> ( A e. On /\ A. x ( Lim x -> A e. x ) ) )
2		limom	|- Lim _om
3		omex	|- _om e. _V
4		limeq	|- ( x = _om -> ( Lim x <-> Lim _om ) )
5		eleq2	|- ( x = _om -> ( A e. x <-> A e. _om ) )
6	4 5	imbi12d	|- ( x = _om -> ( ( Lim x -> A e. x ) <-> ( Lim _om -> A e. _om ) ) )
7	3 6	spcv	|- ( A. x ( Lim x -> A e. x ) -> ( Lim _om -> A e. _om ) )
8	2 7	mpi	|- ( A. x ( Lim x -> A e. x ) -> A e. _om )
9		nnon	|- ( A e. _om -> A e. On )
10	8 9	syl	|- ( A. x ( Lim x -> A e. x ) -> A e. On )
11	10	pm4.71ri	|- ( A. x ( Lim x -> A e. x ) <-> ( A e. On /\ A. x ( Lim x -> A e. x ) ) )
12	1 11	bitr4i	|- ( A e. _om <-> A. x ( Lim x -> A e. x ) )