Colors of
variables: wff set class |
Syntax hints: wa 104
wex 1492
wcel 2148
cab 2163
wral 2455
cvv 2737
c0 3422
cint 3844
csuc 4365
com 4589 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 709
ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-ext 2159 ax-sep 4121 ax-iinf 4587 |
This theorem depends on definitions:
df-bi 117 df-tru 1356 df-nf 1461 df-sb 1763 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-ral 2460 df-v 2739 df-in 3135 df-ss 3142 df-int 3845 df-iom 4590 |
This theorem is referenced by: peano5
4597 omelon
4608 frecex
6394 frecabex
6398 fict
6867 infnfi
6894 ominf
6895 inffiexmid
6905 omp1eom
7093 difinfsn
7098 0ct
7105 ctmlemr
7106 ctssdclemn0
7108 ctssdclemr
7110 ctssdc
7111 enumct
7113 omct
7115 ctfoex
7116 nninfex
7119 infnninf
7121 infnninfOLD
7122 nnnninf
7123 exmidlpo
7140 nninfdcinf
7168 nninfwlporlem
7170 nninfwlpoimlemg
7172 nninfwlpoim
7175 cc2lem
7264 niex
7310 enq0ex
7437 nq0ex
7438 uzenom
10424 frecfzennn
10425 nnenom
10433 fxnn0nninf
10437 0tonninf
10438 1tonninf
10439 inftonninf
10440 hashinfuni
10756 hashinfom
10757 xpct
12396 ennnfonelemj0
12401 ennnfonelemg
12403 ennnfonelemen
12421 ctiunct
12440 omctfn
12443 ssomct
12445 bj-charfunbi
14533 subctctexmid
14720 0nninf
14723 nnsf
14724 peano4nninf
14725 peano3nninf
14726 nninfself
14732 nninfsellemeq
14733 nninfsellemeqinf
14735 sbthom
14744 |