![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > funfn | Structured version Visualization version GIF version |
Description: A class is a function if and only if it is a function on its domain. (Contributed by NM, 13-Aug-2004.) |
Ref | Expression |
---|---|
funfn | ⊢ (Fun 𝐴 ↔ 𝐴 Fn dom 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2725 | . . 3 ⊢ dom 𝐴 = dom 𝐴 | |
2 | 1 | biantru 528 | . 2 ⊢ (Fun 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴)) |
3 | df-fn 6552 | . 2 ⊢ (𝐴 Fn dom 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴)) | |
4 | 2, 3 | bitr4i 277 | 1 ⊢ (Fun 𝐴 ↔ 𝐴 Fn dom 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ wa 394 = wceq 1533 dom cdm 5678 Fun wfun 6543 Fn wfn 6544 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-9 2108 ax-ext 2696 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1774 df-cleq 2717 df-fn 6552 |
This theorem is referenced by: funfnd 6585 funssxp 6752 funforn 6817 funbrfvb 6951 funopfvb 6952 ssimaex 6982 fvco 6995 fvco4i 6998 eqfunfv 7044 fvimacnvi 7060 unpreima 7071 respreima 7074 elrnrexdm 7098 elrnrexdmb 7099 ffvresb 7134 funiun 7156 funressn 7168 funresdfunsn 7198 funex 7231 elunirn 7261 suppval1 8171 funsssuppss 8195 smores 8373 rdgsucg 8444 rdglimg 8446 imafi 9200 fundmfibi 9357 residfi 9359 mptfi 9377 ordtypelem6 9548 ordtypelem7 9549 harwdom 9616 ackbij2 10268 mptct 10563 smobeth 10611 hashkf 14327 hashfun 14432 fclim 15533 coapm 18063 psgnghm 21529 lindfrn 21772 elno3 27634 noextenddif 27647 noextendlt 27648 noextendgt 27649 nosupbnd2lem1 27694 noetasuplem4 27715 ausgrumgri 29052 dfnbgr3 29223 wlkiswwlks1 29750 vdn0conngrumgrv2 30078 hlimf 31119 adj1o 31776 abrexdomjm 32380 iunpreima 32434 fresf1o 32497 unipreima 32511 xppreima 32513 suppiniseg 32548 fdifsuppconst 32551 ressupprn 32552 mptctf 32581 orvcval2 34209 fineqvac 34848 fullfunfnv 35673 fullfunfv 35674 abrexdom 37334 diaf11N 40652 dibf11N 40764 imadomfi 41605 gneispace3 43705 fresfo 46568 funbrafvb 46674 funopafvb 46675 funbrafv22b 46768 funopafv2b 46769 dfclnbgr3 47302 grimuhgr 47362 |
Copyright terms: Public domain | W3C validator |