Theorem dfom5b

Description: A quantifier-free definition of _om that does not depend on ax-inf . (Note: label was changed from dfom5 to dfom5b to prevent naming conflict. NM, 12-Feb-2013.) (Contributed by Scott Fenton, 11-Apr-2012)

	Ref	Expression
Assertion	dfom5b	|- _om = ( On i^i |^| Limits )

Proof

Step	Hyp	Ref	Expression
1		vex	|- x e. _V
2	1	elint	|- ( x e. |^| Limits <-> A. y ( y e. Limits -> x e. y ) )
3		vex	|- y e. _V
4	3	ellimits	|- ( y e. Limits <-> Lim y )
5	4	imbi1i	|- ( ( y e. Limits -> x e. y ) <-> ( Lim y -> x e. y ) )
6	5	albii	|- ( A. y ( y e. Limits -> x e. y ) <-> A. y ( Lim y -> x e. y ) )
7	2 6	bitr2i	|- ( A. y ( Lim y -> x e. y ) <-> x e. |^| Limits )
8	7	anbi2i	|- ( ( x e. On /\ A. y ( Lim y -> x e. y ) ) <-> ( x e. On /\ x e. |^| Limits ) )
9		elom	|- ( x e. _om <-> ( x e. On /\ A. y ( Lim y -> x e. y ) ) )
10		elin	|- ( x e. ( On i^i |^| Limits ) <-> ( x e. On /\ x e. |^| Limits ) )
11	8 9 10	3bitr4i	|- ( x e. _om <-> x e. ( On i^i |^| Limits ) )
12	11	eqriv	|- _om = ( On i^i |^| Limits )