Metamath Proof Explorer


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 xψ
onminsb.2 x=xOn|φφψ
Assertion onminsb xOnφψ

Proof

Step Hyp Ref Expression
1 onminsb.1 xψ
2 onminsb.2 x=xOn|φφψ
3 rabn0 xOn|φxOnφ
4 ssrab2 xOn|φOn
5 onint xOn|φOnxOn|φxOn|φxOn|φ
6 4 5 mpan xOn|φxOn|φxOn|φ
7 3 6 sylbir xOnφxOn|φxOn|φ
8 nfrab1 _xxOn|φ
9 8 nfint _xxOn|φ
10 nfcv _xOn
11 9 10 1 2 elrabf xOn|φxOn|φxOn|φOnψ
12 11 simprbi xOn|φxOn|φψ
13 7 12 syl xOnφψ