![]() |
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 2760 | . . 3 ⊢ dom 𝐴 = dom 𝐴 | |
2 | 1 | biantru 527 | . 2 ⊢ (Fun 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴)) |
3 | df-fn 6052 | . 2 ⊢ (𝐴 Fn dom 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴)) | |
4 | 2, 3 | bitr4i 267 | 1 ⊢ (Fun 𝐴 ↔ 𝐴 Fn dom 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 ∧ wa 383 = 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 ax-gen 1871 ax-4 1886 ax-5 1988 ax-6 2054 ax-7 2090 ax-9 2148 ax-ext 2740 |
This theorem depends on definitions: df-bi 197 df-an 385 df-ex 1854 df-cleq 2753 df-fn 6052 |
This theorem is referenced by: funfnd 6080 funssxp 6222 funforn 6284 funbrfvb 6400 funopfvb 6401 ssimaex 6426 fvco 6437 fvco4i 6439 eqfunfv 6480 fvimacnvi 6495 unpreima 6505 respreima 6508 elrnrexdm 6527 elrnrexdmb 6528 ffvresb 6558 funiun 6576 funressn 6590 funresdfunsn 6620 resfunexg 6644 funex 6647 funiunfv 6670 elunirn 6673 suppval1 7470 funsssuppss 7491 wfrlem4 7588 smores 7619 smores2 7621 tfrlem1 7642 rdgsucg 7689 rdglimg 7691 fundmfibi 8412 resfnfinfin 8413 residfi 8414 mptfi 8432 resfifsupp 8470 ordtypelem4 8593 ordtypelem6 8595 ordtypelem7 8596 ordtypelem9 8598 ordtypelem10 8599 harwdom 8662 ackbij2 9277 brdom3 9562 brdom5 9563 brdom4 9564 mptct 9572 smobeth 9620 fpwwe2lem11 9674 hashkf 13333 hashfun 13436 hashimarn 13439 resunimafz0 13441 fclim 14503 isstruct2 16089 xpsc0 16442 xpsc1 16443 invf 16649 coapm 16942 psgnghm 20148 lindfrn 20382 ofco2 20479 dfac14 21643 perfdvf 23886 c1lip2 23980 taylf 24334 lpvtx 26183 upgrle2 26220 uhgrvtxedgiedgb 26251 ausgrumgri 26282 uhgr2edg 26320 ushgredgedg 26341 ushgredgedgloop 26343 subgruhgredgd 26396 subuhgr 26398 subupgr 26399 subumgr 26400 subusgr 26401 dfnbgr3 26451 vtxdun 26608 upgrewlkle2 26733 wlkiswwlks1 26997 vdn0conngrumgrv2 27369 eupthvdres 27408 hlimf 28424 adj1o 29083 abrexdomjm 29673 iunpreima 29711 fresf1o 29763 unipreima 29776 xppreima 29779 mptctf 29825 sitgf 30739 orvcval2 30850 frrlem4 32110 elno3 32135 noextenddif 32148 noextendlt 32149 noextendgt 32150 nosupbnd2lem1 32188 noetalem3 32192 fullfunfnv 32380 fullfunfv 32381 abrexdom 33856 diaf11N 36858 dibf11N 36970 gneispace3 38951 gneispace 38952 gneispacef2 38954 funcoressn 41731 funbrafvb 41760 funopafvb 41761 |
Copyright terms: Public domain | W3C validator |