Colors of
variables: wff
setvar class |
Syntax hints:
≠ wne 2941 ∅c0 4323
suc csuc 6367 1oc1o 8459 2oc2o 8460 |
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 5307 |
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-ne 2942 df-v 3477 df-dif 3952 df-un 3954 df-nul 4324 df-sn 4630 df-suc 6371 df-2o 8467 |
This theorem is referenced by: ord2eln012
8497 snnen2oOLD
9227 snnen2o
9237 1sdom2
9240 1sdom2dom
9247 pmtrfmvdn0
19330 pmtrsn
19387 efgrcl
19583 sltval2
27159 sltintdifex
27164 nogt01o
27199 noinfbnd1lem5
27230 noinfbnd2lem1
27233 goaln0
34384 goalr
34388 fmla0disjsuc
34389 onint1
35334 1oequni2o
36249 finxpreclem4
36275 finxp3o
36281 frlmpwfi
41840 clsk1indlem1
42796 |