Colors of
variables: wff
setvar class |
Syntax hints:
∈ wcel 2107 Ord word 6364
Oncon0 6365 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914
ax-6 1972 ax-7 2012 ax-8 2109
ax-9 2117 ax-ext 2704 |
This theorem depends on definitions:
df-bi 206 df-an 398
df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-ral 3063 df-v 3477 df-in 3956 df-ss 3966 df-uni 4910 df-tr 5267 df-po 5589 df-so 5590 df-fr 5632 df-we 5634 df-ord 6368 df-on 6369 |
This theorem is referenced by: onirri
6478 onsucssi
7830 ord1eln01
8496 ord2eln012
8497 oawordeulem
8554 omopthi
8660 en2
9281 en3
9282 ssttrcl
9710 ttrcltr
9711 dmttrcl
9716 ttrclselem2
9721 bndrank
9836 rankprb
9846 rankuniss
9861 rankelun
9867 rankelpr
9868 rankelop
9869 rankmapu
9873 rankxplim3
9876 rankxpsuc
9877 cardlim
9967 carduni
9976 dfac8b
10026 alephdom2
10082 alephfp
10103 dfac12lem2
10139 dju1p1e2ALT
10169 cfsmolem
10265 ttukeylem6
10509 ttukeylem7
10510 unsnen
10548 efgmnvl
19582 nogt01o
27199 scutbdaybnd2lim
27319 slerec
27321 bday1s
27333 cuteq1
27335 newbday
27397 negsproplem7
27511 mulsproplem13
27587 mulsproplem14
27588 sltonold
27690 hfuni
35187 finxpsuclem
36326 pwfi2f1o
41886 |