![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fnfun | Structured version Visualization version GIF version |
Description: A function with domain is a function. (Contributed by NM, 1-Aug-1994.) |
Ref | Expression |
---|---|
fnfun | ⊢ (𝐹 Fn 𝐴 → Fun 𝐹) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-fn 6052 | . 2 ⊢ (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴)) | |
2 | 1 | simplbi 478 | 1 ⊢ (𝐹 Fn 𝐴 → Fun 𝐹) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1632 dom cdm 5266 Fun wfun 6043 Fn wfn 6044 |
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 197 df-an 385 df-fn 6052 |
This theorem is referenced by: fnrel 6150 funfni 6152 fnco 6160 fnssresb 6164 ffun 6209 f1fun 6264 f1ofun 6300 fnbrfvb 6397 fvelimab 6415 fvun1 6431 elpreima 6500 respreima 6507 fnsnr 6595 fnprb 6636 fntpb 6637 fconst3 6641 fnfvima 6659 fnunirn 6674 nvof1o 6699 f1eqcocnv 6719 fnexALT 7297 curry1 7437 curry2 7440 suppvalfn 7470 suppfnss 7488 suppfnssOLD 7489 fnsuppres 7491 wfrlem2 7584 wfrlem14 7597 tfrlem4 7644 tfrlem5 7645 tfrlem11 7653 tz7.48-2 7706 tz7.49 7709 fndmeng 8199 fnfi 8403 fodomfi 8404 resfnfinfin 8411 fczfsuppd 8458 marypha2lem4 8509 inf0 8691 r1elss 8842 dfac8alem 9042 alephfp 9121 dfac3 9134 dfac9 9150 dfac12lem1 9157 dfac12lem2 9158 r1om 9258 cfsmolem 9284 alephsing 9290 zorn2lem1 9510 zorn2lem5 9514 zorn2lem6 9515 zorn2lem7 9516 ttukeylem3 9525 ttukeylem6 9528 fnct 9551 smobeth 9600 fpwwe2lem9 9652 wunr1om 9733 tskr1om 9781 tskr1om2 9782 uzrdg0i 12952 uzrdgsuci 12953 hashkf 13313 cshimadifsn 13775 cshimadifsn0 13776 shftfn 14012 phimullem 15686 imasaddvallem 16391 imasvscaval 16400 frmdss2 17601 lcomfsupp 19105 lidlval 19394 rspval 19395 psrbagev1 19712 psgnghm 20128 frlmsslsp 20337 iscldtop 21101 2ndcomap 21463 qtoptop 21705 basqtop 21716 qtoprest 21722 kqfvima 21735 isr0 21742 kqreglem1 21746 kqnrmlem1 21748 kqnrmlem2 21749 elrnust 22229 ustbas 22232 uniiccdif 23546 fcoinver 29725 mdetpmtr1 30198 fimaproj 30209 sseqf 30763 sseqfv2 30765 elorrvc 30834 bnj930 31147 bnj1371 31404 bnj1497 31435 frrlem2 32087 noextendseq 32126 madeval 32241 filnetlem4 32682 heibor1lem 33921 diaf11N 36840 dibf11N 36952 dibclN 36953 dihintcl 37135 ismrc 37766 dnnumch1 38116 aomclem4 38129 aomclem6 38131 ntrclsfv1 38855 ntrneifv1 38879 fvelimad 39957 fnfvimad 39958 fvelima2 39974 climrescn 40483 icccncfext 40603 stoweidlem29 40749 stoweidlem59 40779 ovolval4lem1 41369 fnresfnco 41712 funcoressn 41713 fnbrafvb 41740 tz6.12-afv 41759 afvco2 41762 plusfreseq 42282 dfrngc2 42482 dfringc2 42528 rngcresringcat 42540 mndpsuppss 42662 mndpfsupp 42667 |
Copyright terms: Public domain | W3C validator |