Theorem onminesb

Description: If a property is true for some ordinal number, it is true for a minimal ordinal number. This version uses explicit substitution. Theorem Schema 62 of Suppes p. 228. (Contributed by NM, 29-Sep-2003)

	Ref	Expression
Assertion	onminesb	|- ( E. x e. On ph -> [. |^| { x e. On | ph } / x ]. ph )

Proof

Step	Hyp	Ref	Expression
1		rabn0	|- ( { x e. On | ph } =/= (/) <-> E. x e. On ph )
2		ssrab2	|- { x e. On | ph } C_ On
3		onint	|- ( ( { x e. On | ph } C_ On /\ { x e. On | ph } =/= (/) ) -> |^| { x e. On | ph } e. { x e. On | ph } )
4	2 3	mpan	|- ( { x e. On | ph } =/= (/) -> |^| { x e. On | ph } e. { x e. On | ph } )
5	1 4	sylbir	|- ( E. x e. On ph -> |^| { x e. On | ph } e. { x e. On | ph } )
6		nfcv	|- F/_ x On
7	6	elrabsf	|- ( |^| { x e. On | ph } e. { x e. On | ph } <-> ( |^| { x e. On | ph } e. On /\ [. |^| { x e. On | ph } / x ]. ph ) )
8	7	simprbi	|- ( |^| { x e. On | ph } e. { x e. On | ph } -> [. |^| { x e. On | ph } / x ]. ph )
9	5 8	syl	|- ( E. x e. On ph -> [. |^| { x e. On | ph } / x ]. ph )