Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ↔ wb 205
∧ wa 395 ∈
wcel 2098 ⊆ wss 3943
Ord word 6357 suc csuc 6360 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905
ax-6 1963 ax-7 2003 ax-8 2100
ax-9 2108 ax-ext 2697 ax-sep 5292 ax-nul 5299 ax-pr 5420 |
This theorem depends on definitions:
df-bi 206 df-an 396
df-or 845 df-3or 1085 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-sb 2060 df-clab 2704 df-cleq 2718 df-clel 2804 df-ne 2935 df-ral 3056 df-rex 3065 df-rab 3427 df-v 3470 df-dif 3946 df-un 3948 df-in 3950 df-ss 3960 df-pss 3962 df-nul 4318 df-if 4524 df-pw 4599 df-sn 4624 df-pr 4626 df-op 4630 df-uni 4903 df-br 5142 df-opab 5204 df-tr 5259 df-eprel 5573 df-po 5581 df-so 5582 df-fr 5624 df-we 5626 df-ord 6361 df-on 6362 df-suc 6364 |
This theorem is referenced by: onsucmin
7806 onsucssi
7827 tfindsg2
7848 ordgt0ge1
8494 onomeneqOLD
9231 cantnflem1
9686 ttrcltr
9713 dmttrcl
9718 r1ordg
9775 r1val1
9783 rankonidlem
9825 rankxplim3
9878 ordeldifsucon
42582 ordeldif1o
42583 oaltom
42729 omltoe
42731 |