Description: If a wff is true for an ordinal number, then there is the smallest ordinal number for which it is true. (Contributed by NM, 2-Feb-1997) (Proof shortened by Mario Carneiro, 20-Nov-2016)
Ref | Expression | ||
---|---|---|---|
Hypothesis | onminex.1 | |
|
Assertion | onminex | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | onminex.1 | |
|
2 | ssrab2 | |
|
3 | rabn0 | |
|
4 | 3 | biimpri | |
5 | oninton | |
|
6 | 2 4 5 | sylancr | |
7 | onminesb | |
|
8 | onss | |
|
9 | 6 8 | syl | |
10 | 9 | sseld | |
11 | 1 | onnminsb | |
12 | 10 11 | syli | |
13 | 12 | ralrimiv | |
14 | dfsbcq2 | |
|
15 | raleq | |
|
16 | 14 15 | anbi12d | |
17 | 16 | rspcev | |
18 | 6 7 13 17 | syl12anc | |
19 | nfv | |
|
20 | nfs1v | |
|
21 | nfv | |
|
22 | 20 21 | nfan | |
23 | sbequ12 | |
|
24 | raleq | |
|
25 | 23 24 | anbi12d | |
26 | 19 22 25 | cbvrexw | |
27 | 18 26 | sylibr | |