Theorem onminsb

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

	Ref	Expression
Hypotheses	onminsb.1	|- F/ x ps
	onminsb.2	|- ( x = |^| { x e. On | ph } -> ( ph <-> ps ) )
Assertion	onminsb	|- ( E. x e. On ph -> ps )

Proof

Step	Hyp	Ref	Expression
1		onminsb.1	|- F/ x ps
2		onminsb.2	|- ( x = |^| { x e. On | ph } -> ( ph <-> ps ) )
3		rabn0	|- ( { x e. On | ph } =/= (/) <-> E. x e. On ph )
4		ssrab2	|- { x e. On | ph } C_ On
5		onint	|- ( ( { x e. On | ph } C_ On /\ { x e. On | ph } =/= (/) ) -> |^| { x e. On | ph } e. { x e. On | ph } )
6	4 5	mpan	|- ( { x e. On | ph } =/= (/) -> |^| { x e. On | ph } e. { x e. On | ph } )
7	3 6	sylbir	|- ( E. x e. On ph -> |^| { x e. On | ph } e. { x e. On | ph } )
8		nfrab1	|- F/_ x { x e. On | ph }
9	8	nfint	|- F/_ x |^| { x e. On | ph }
10		nfcv	|- F/_ x On
11	9 10 1 2	elrabf	|- ( |^| { x e. On | ph } e. { x e. On | ph } <-> ( |^| { x e. On | ph } e. On /\ ps ) )
12	11	simprbi	|- ( |^| { x e. On | ph } e. { x e. On | ph } -> ps )
13	7 12	syl	|- ( E. x e. On ph -> ps )