Colors of
variables: wff
setvar class |
Syntax hints:
≠ wne 2944 ∅c0 4283
suc csuc 6320 1oc1o 8406 2oc2o 8407 |
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 2708 ax-nul 5264 |
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 2715 df-cleq 2729 df-clel 2815 df-ne 2945 df-v 3448 df-dif 3914 df-un 3916 df-nul 4284 df-sn 4588 df-suc 6324 df-2o 8414 |
This theorem is referenced by: ord2eln012
8444 snnen2oOLD
9172 snnen2o
9182 1sdom2
9185 1sdom2dom
9192 pmtrfmvdn0
19245 pmtrsn
19302 efgrcl
19498 sltval2
27007 sltintdifex
27012 nogt01o
27047 noinfbnd1lem5
27078 noinfbnd2lem1
27081 goaln0
33990 goalr
33994 fmla0disjsuc
33995 onint1
34924 1oequni2o
35842 finxpreclem4
35868 finxp3o
35874 frlmpwfi
41428 clsk1indlem1
42324 |