Theorem onintrab

Description: The intersection of a class of ordinal numbers exists iff it is an ordinal number. (Contributed by NM, 6-Nov-2003)

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

Proof

Step	Hyp	Ref	Expression
1		intex	|- ( { x e. On | ph } =/= (/) <-> |^| { x e. On | ph } e. _V )
2		ssrab2	|- { x e. On | ph } C_ On
3		oninton	|- ( ( { x e. On | ph } C_ On /\ { x e. On | ph } =/= (/) ) -> |^| { x e. On | ph } e. On )
4	2 3	mpan	|- ( { x e. On | ph } =/= (/) -> |^| { x e. On | ph } e. On )
5	1 4	sylbir	|- ( |^| { x e. On | ph } e. _V -> |^| { x e. On | ph } e. On )
6		elex	|- ( |^| { x e. On | ph } e. On -> |^| { x e. On | ph } e. _V )
7	5 6	impbii	|- ( |^| { x e. On | ph } e. _V <-> |^| { x e. On | ph } e. On )