Colors of
variables: wff set class |
Syntax hints: wi 4
wceq 1353
cin 3128 |
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 |
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-v 2739 df-in 3135 |
This theorem is referenced by: disjpr2
3656 rint0
3883 riin0
3958 disji2
3996 xpriindim
4765 riinint
4888 reseq2
4902 csbresg
4910 resindm
4949 isoselem
5820 zfz1isolem1
10819 fsumm1
11423 ennnfonelemhf1o
12413 nninfdclemcl
12448 nninfdclemp1
12450 nninfdc
12453 ressvalsets
12523 ressbasd
12526 ressinbasd
12532 ressressg
12533 restval
12693 mgpress
13139 subrgpropd
13367 basis1
13517 baspartn
13520 eltg
13522 tgdom
13542 ntrval
13580 resttopon2
13648 restopnb
13651 qtopbasss
13991 |