Colors of
variables: wff set class |
Syntax hints: wa 104
wb 105 wal 1351 wceq 1353 wex 1490 wcel 2146 cvv 2735 cin 3126 |
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 1445 ax-7 1446 ax-gen 1447 ax-ie1 1491 ax-ie2 1492 ax-8 1502 ax-10 1503 ax-11 1504 ax-i12 1505 ax-bndl 1507 ax-4 1508 ax-17 1524 ax-i9 1528 ax-ial 1532 ax-i5r 1533 ax-ext 2157 ax-sep 4116 |
This theorem depends on definitions:
df-bi 117 df-tru 1356 df-nf 1459 df-sb 1761 df-clab 2162 df-cleq 2168 df-clel 2171 df-nfc 2306 df-v 2737 df-in 3133 |
This theorem is referenced by: inex2
4133 inex1g
4134 inuni
4150 bnd2
4168 peano5
4591 ssimaex
5569 ofmres
6127 tfrexlem
6325 elrest
12616 epttop
13083 tgrest
13162 resttopon
13164 restco
13167 cnrest2
13229 cnptopresti
13231 cnptoprest
13232 cnptoprest2
13233 txrest
13269 |