Theorem onintrab2

Description: An existence condition equivalent to an intersection's being an ordinal number. (Contributed by NM, 6-Nov-2003)

	Ref	Expression
Assertion	onintrab2	|- ( E. x e. On ph <-> |^| { x e. On | ph } e. On )

Proof

Step	Hyp	Ref	Expression
1		intexrab	|- ( E. x e. On ph <-> |^| { x e. On | ph } e. _V )
2		onintrab	|- ( |^| { x e. On | ph } e. _V <-> |^| { x e. On | ph } e. On )
3	1 2	bitri	|- ( E. x e. On ph <-> |^| { x e. On | ph } e. On )