Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ↔ wb 205
∈ wcel 2106 Ord word 6314
Oncon0 6315 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913
ax-6 1971 ax-7 2011 ax-8 2108
ax-9 2116 ax-ext 2707 |
This theorem depends on definitions:
df-bi 206 df-an 397
df-tru 1544 df-ex 1782 df-sb 2068 df-clab 2714 df-cleq 2728 df-clel 2814 df-ral 3063 df-v 3445 df-in 3915 df-ss 3925 df-uni 4864 df-tr 5221 df-po 5543 df-so 5544 df-fr 5586 df-we 5588 df-ord 6318 df-on 6319 |
This theorem is referenced by: elon
6324 eloni
6325 elon2
6326 ordelon
6339 onin
6346 limelon
6379 ordsssuc2
6406 onprc
7708 ssonuni
7710 sucexeloni
7740 sucexeloniOLD
7741 suceloniOLD
7743 ordsucOLD
7745 cofon1
8614 cofon2
8615 enp1i
9219 oion
9468 hartogs
9476 card2on
9486 tskwe
9882 onssnum
9972 hsmexlem1
10358 ondomon
10495 1stcrestlem
22787 nosupno
27035 noinfno
27050 hfninf
34738 rn1st
43439 |