Colors of
variables: wff
setvar class |
Syntax hints:
↔ wb 205 = wceq 1542
∈ wcel 2107 ∅c0 4286 {csn 4590
1oc1o 8409 |
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 ax-nul 5267 |
This theorem depends on definitions:
df-bi 206 df-an 398
df-or 847 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-v 3449 df-dif 3917 df-un 3919 df-nul 4287 df-sn 4591 df-suc 6327 df-1o 8416 |
This theorem is referenced by: ord1eln01
8446 ord2eln012
8447 0lt1o
8454 oelim2
8546 oeeulem
8552 oaabs2
8599 cantnff
9618 cnfcom3lem
9647 cfsuc
10201 pf1ind
21744 mavmul0
21924 cramer0
22062 cantnfresb
41706 omabs2
41714 omcl3g
41716 f1omo
47017 |