![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > fnfun | Structured version Unicode version |
Description: A function with domain is a function. (Contributed by NM, 1-Aug-1994.) |
Ref | Expression |
---|---|
fnfun |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-fn 5528 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | simplbi 460 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 185 df-an 371 df-fn 5528 |
This theorem is referenced by: fnrel 5616 funfni 5618 fnco 5626 fnssresb 5630 ffun 5668 f1fun 5715 f1ofun 5750 fnbrfvb 5840 fvelimab 5855 fvun1 5870 elpreima 5931 respreima 5940 fnsnb 6006 fnprb 6044 fnprOLD 6045 fconst3 6049 fnfvima 6063 fnunirn 6078 nvof1o 6095 f1eqcocnv 6107 fnexALT 6652 curry1 6773 curry2 6776 suppvalfn 6806 suppfnss 6823 fnsuppres 6825 tfrlem4 6947 tfrlem5 6948 tfrlem11 6956 tz7.48-2 7006 tz7.49 7009 fndmeng 7495 fnfi 7699 fodomfi 7700 fczfsuppd 7748 marypha2lem4 7798 inf0 7937 noinfepOLD 7976 r1elss 8123 dfac8alem 8309 alephfp 8388 dfac3 8401 dfac9 8415 dfac12lem1 8422 dfac12lem2 8423 r1om 8523 cfsmolem 8549 alephsing 8555 zorn2lem1 8775 zorn2lem5 8779 zorn2lem6 8780 zorn2lem7 8781 ttukeylem3 8790 ttukeylem6 8793 smobeth 8860 fpwwe2lem9 8915 wunr1om 8996 tskr1om 9044 tskr1om2 9045 uzrdg0i 11898 uzrdgsuci 11899 hashkf 12221 shftfn 12679 phimullem 13971 imasaddvallem 14585 imasvscaval 14594 frmdss2 15659 dprdvalOLD 16608 lcomfsupp 17107 lidlval 17395 rspval 17396 psrbagev1 17717 psgnghm 18134 frlmsslsp 18347 frlmsslspOLD 18348 iscldtop 18830 2ndcomap 19193 qtoptop 19404 basqtop 19415 qtoprest 19421 kqfvima 19434 isr0 19441 kqreglem1 19445 kqnrmlem1 19447 kqnrmlem2 19448 elrnust 19930 ustbas 19933 uniiccdif 21190 eupap1 23748 fnct 26163 sseqf 26918 sseqfv2 26920 elorrvc 26989 wfrlem2 27868 wfrlem14 27880 frrlem2 27912 bpolylem 28334 filnetlem4 28749 heibor1lem 28855 ismrc 29184 dnnumch1 29544 aomclem4 29557 aomclem6 29559 stoweidlem29 29971 stoweidlem59 30001 fnresfnco 30179 funcoressn 30180 fnbrafvb 30207 tz6.12-afv 30226 afvco2 30229 resfnfinfin 30312 mndpsuppss 30931 mndpfsupp 30937 bnj142OLD 32034 bnj930 32080 bnj1371 32337 bnj1497 32368 diaf11N 35017 dibf11N 35129 dibclN 35130 dihintcl 35312 |
Copyright terms: Public domain | W3C validator |