| 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 2737 | . . 3 ⊢ dom 𝐴 = dom 𝐴 | |
| 2 | 1 | biantru 529 | . 2 ⊢ (Fun 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴)) |
| 3 | df-fn 6564 | . 2 ⊢ (𝐴 Fn dom 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴)) | |
| 4 | 2, 3 | bitr4i 278 | 1 ⊢ (Fun 𝐴 ↔ 𝐴 Fn dom 𝐴) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 ∧ wa 395 = wceq 1540 dom cdm 5685 Fun wfun 6555 Fn wfn 6556 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-cleq 2729 df-fn 6564 |
| This theorem is referenced by: funfnd 6597 funssxp 6764 funforn 6827 funbrfvb 6962 funopfvb 6963 ssimaex 6994 fvco 7007 fvco4i 7010 eqfunfv 7056 fvimacnvi 7072 unpreima 7083 respreima 7086 elrnrexdm 7109 elrnrexdmb 7110 ffvresb 7145 funiun 7167 funressn 7179 funresdfunsn 7209 funex 7239 elunirn 7271 suppval1 8191 funsssuppss 8215 smores 8392 rdgsucg 8463 rdglimg 8465 imafiOLD 9354 fundmfibi 9376 residfi 9378 mptfi 9391 ordtypelem6 9563 ordtypelem7 9564 harwdom 9631 ackbij2 10282 mptct 10578 smobeth 10626 hashkf 14371 hashfun 14476 fclim 15589 coapm 18116 psgnghm 21598 lindfrn 21841 elno3 27700 noextenddif 27713 noextendlt 27714 noextendgt 27715 nosupbnd2lem1 27760 noetasuplem4 27781 ausgrumgri 29184 dfnbgr3 29355 wlkiswwlks1 29887 vdn0conngrumgrv2 30215 hlimf 31256 adj1o 31913 abrexdomjm 32526 iunpreima 32577 fresf1o 32641 unipreima 32653 xppreima 32655 suppiniseg 32695 fdifsuppconst 32698 ressupprn 32699 mptctf 32729 orvcval2 34461 fineqvac 35111 fullfunfnv 35947 fullfunfv 35948 abrexdom 37737 diaf11N 41051 dibf11N 41163 imadomfi 42003 gneispace3 44146 fresfo 47060 funbrafvb 47168 funopafvb 47169 funbrafv22b 47262 funopafv2b 47263 dfclnbgr3 47813 grimuhgr 47878 |
| Copyright terms: Public domain | W3C validator |