Colors of
variables: wff
setvar class |
Syntax hints:
= wceq 1542 ∪ cun 3909
∅c0 4283 {csn 4587
{cpr 4589 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 |
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-v 3448 df-dif 3914 df-un 3916 df-nul 4284 df-pr 4590 df-suc 6324 df-1o 8413 df-2o 8414 |
This theorem is referenced by: df2o2
8422 2oex
8424 nlim2
8437 ord2eln012
8444 2oconcl
8450 enpr2d
8994 map2xp
9092 snnen2o
9182 rex2dom
9191 1sdom2dom
9192 1sdomOLD
9194 cantnflem2
9627 xp2dju
10113 sdom2en01
10239 sadcf
16334 fnpr2o
17440 fnpr2ob
17441 fvprif
17444 xpsfrnel
17445 xpsfeq
17446 xpsle
17462 setcepi
17975 setc2obas
17981 setc2ohom
17982 efgi0
19503 efgi1
19504 vrgpf
19551 vrgpinv
19552 frgpuptinv
19554 frgpup2
19559 frgpup3lem
19560 frgpnabllem1
19652 dmdprdpr
19829 dprdpr
19830 xpstopnlem1
23163 xpstopnlem2
23165 xpsxmetlem
23735 xpsdsval
23737 xpsmet
23738 onint1
34924 pw2f1ocnv
41364 wepwsolem
41372 omnord1ex
41641 oege2
41644 df3o2
41650 oenord1ex
41652 oenord1
41653 oaomoencom
41654 oenassex
41655 omabs2
41668 omcl3g
41670 clsk1independent
42325 |