Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ⊆ wss 3949
↾ cres 5679 Fun wfun 6538 |
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 2704 |
This theorem depends on definitions:
df-bi 206 df-an 398
df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-v 3477 df-in 3956 df-ss 3966 df-br 5150 df-opab 5212 df-rel 5684 df-cnv 5685 df-co 5686 df-res 5689 df-fun 6546 |
This theorem is referenced by: funresd
6592 fores
6816 resfunexg
7217 funfvima
7232 funiunfv
7247 fprlem1
8285 wfrlem5OLD
8313 smores
8352 smores2
8354 frfnom
8435 sbthlem7
9089 fsuppres
9388 ordtypelem4
9516 wdomima2g
9581 imadomg
10529 hashres
14398 hashimarn
14400 setsfun
17104 setsfun0
17105 lubfun
18305 glbfun
18318 qtoptop2
23203 volf
25046 nolesgn2ores
27175 nosupres
27210 nosupbnd2lem1
27218 noetasuplem4
27239 noetainflem4
27243 uhgrspansubgrlem
28547 upgrres
28563 umgrres
28564 hlimf
30490 fsuppcurry1
31950 fsuppcurry2
31951 eulerpartlemmf
33374 eulerpartlemgvv
33375 bj-funidres
36032 funcoressn
45752 fundmdfat
45837 afvelrn
45876 dmfcoafv
45883 aovmpt4g
45909 fundmafv2rnb
45938 |