Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > funfn | Structured version Visualization version GIF version |
Description: An equivalence for the function predicate. (Contributed by NM, 13-Aug-2004.) |
Ref | Expression |
---|---|
funfn | ⊢ (Fun 𝐴 ↔ 𝐴 Fn dom 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2610 | . . 3 ⊢ dom 𝐴 = dom 𝐴 | |
2 | 1 | biantru 525 | . 2 ⊢ (Fun 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴)) |
3 | df-fn 5807 | . 2 ⊢ (𝐴 Fn dom 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴)) | |
4 | 2, 3 | bitr4i 266 | 1 ⊢ (Fun 𝐴 ↔ 𝐴 Fn dom 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 195 ∧ wa 383 = wceq 1475 dom cdm 5038 Fun wfun 5798 Fn wfn 5799 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-an 385 df-cleq 2603 df-fn 5807 |
This theorem is referenced by: funssxp 5974 funforn 6035 funbrfvb 6148 funopfvb 6149 ssimaex 6173 fvco 6184 fvco4i 6186 eqfunfv 6224 fvimacnvi 6239 unpreima 6249 respreima 6252 elrnrexdm 6271 elrnrexdmb 6272 ffvresb 6301 funiun 6318 funressn 6331 funresdfunsn 6360 resfunexg 6384 funex 6387 funiunfv 6410 elunirn 6413 suppval1 7188 funsssuppss 7208 wfrlem4 7305 smores 7336 smores2 7338 tfrlem1 7359 rdgsucg 7406 rdglimg 7408 fundmfibi 8130 mptfi 8148 resfifsupp 8186 ordtypelem4 8309 ordtypelem6 8311 ordtypelem7 8312 ordtypelem9 8314 ordtypelem10 8315 harwdom 8378 ackbij2 8948 brdom3 9231 brdom5 9232 brdom4 9233 smobeth 9287 fpwwe2lem11 9341 hashkf 12981 hashfun 13084 hashimarn 13085 fclim 14132 isstruct2 15704 xpsc0 16043 xpsc1 16044 invf 16251 coapm 16544 psgnghm 19745 lindfrn 19979 ofco2 20076 dfac14 21231 perfdvf 23473 c1lip2 23565 taylf 23919 lpvtx 25734 upgrle2 25771 uhgrvtxedgiedgb 25810 usgra2edg 25911 usgrarnedg 25913 usgrafilem2 25941 cusgrares 26001 vdusgraval 26434 vdgrnn0pnf 26436 vdn0frgrav2 26550 vdgn0frgrav2 26551 vdgfrgragt2 26554 hlimf 27478 adj1o 28137 abrexdomjm 28729 iunpreima 28765 fresf1o 28815 unipreima 28826 xppreima 28829 mptct 28880 mptctf 28883 sitgf 29736 orvcval2 29847 frrlem4 31027 elno3 31052 fullfunfnv 31223 fullfunfv 31224 abrexdom 32695 diaf11N 35356 dibf11N 35468 gneispace3 37451 gneispace 37452 gneispacef2 37454 funcoressn 39856 funbrafvb 39885 funopafvb 39886 resfnfinfin 40339 residfi 40340 resunimafz0 40368 ausgrumgri 40397 uhgr2edg 40435 ushgredgedga 40456 ushgredgedgaloop 40458 subgruhgredgd 40508 subuhgr 40510 subupgr 40511 subumgr 40512 subusgr 40513 dfnbgr3 40562 vtxdun 40696 upgrewlkle2 40808 1wlkiswwlks1 41064 vdn0conngrumgrv2 41363 eupthvdres 41403 |
Copyright terms: Public domain | W3C validator |