Colors of
variables: wff
setvar class |
Syntax hints:
↔ wb 205 = wceq 1534
∈ wcel 2099 ∅c0 4318 {csn 4624
1oc1o 8473 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906
ax-6 1964 ax-7 2004 ax-8 2101
ax-9 2109 ax-ext 2698 ax-nul 5300 |
This theorem depends on definitions:
df-bi 206 df-an 396
df-or 847 df-tru 1537 df-fal 1547 df-ex 1775 df-sb 2061 df-clab 2705 df-cleq 2719 df-clel 2805 df-v 3471 df-dif 3947 df-un 3949 df-nul 4319 df-sn 4625 df-suc 6369 df-1o 8480 |
This theorem is referenced by: ord1eln01
8510 ord2eln012
8511 0lt1o
8518 oelim2
8609 oeeulem
8615 oaabs2
8663 cantnff
9689 cnfcom3lem
9718 cfsuc
10272 pf1ind
22261 mavmul0
22441 cramer0
22579 cantnfresb
42676 omabs2
42684 omcl3g
42686 f1omo
47836 |