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 533 | . 2 ⊢ (Fun 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴)) |
3 | df-fn 6383 | . 2 ⊢ (𝐴 Fn dom 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴)) | |
4 | 2, 3 | bitr4i 281 | 1 ⊢ (Fun 𝐴 ↔ 𝐴 Fn dom 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 209 ∧ wa 399 = wceq 1543 dom cdm 5551 Fun wfun 6374 Fn wfn 6375 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-9 2120 ax-ext 2708 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1788 df-cleq 2729 df-fn 6383 |
This theorem is referenced by: funfnd 6411 funssxp 6574 funforn 6640 funbrfvb 6767 funopfvb 6768 ssimaex 6796 fvco 6809 fvco4i 6812 eqfunfv 6857 fvimacnvi 6872 unpreima 6883 respreima 6886 elrnrexdm 6908 elrnrexdmb 6909 ffvresb 6941 funiun 6962 funressn 6974 funresdfunsn 7004 funex 7035 elunirn 7064 suppval1 7909 funsssuppss 7932 smores 8089 rdgsucg 8159 rdglimg 8161 imafi 8853 fundmfibi 8955 residfi 8957 mptfi 8975 ordtypelem6 9139 ordtypelem7 9140 harwdom 9207 ackbij2 9857 mptct 10152 smobeth 10200 hashkf 13898 hashfun 14004 fclim 15114 coapm 17577 psgnghm 20542 lindfrn 20783 ausgrumgri 27258 dfnbgr3 27426 wlkiswwlks1 27951 vdn0conngrumgrv2 28279 hlimf 29318 adj1o 29975 abrexdomjm 30571 iunpreima 30623 fresf1o 30685 unipreima 30700 xppreima 30702 suppiniseg 30740 fdifsuppconst 30743 ressupprn 30744 mptctf 30772 orvcval2 32137 fineqvac 32779 elno3 33595 noextenddif 33608 noextendlt 33609 noextendgt 33610 nosupbnd2lem1 33655 noetasuplem4 33676 fullfunfnv 33985 fullfunfv 33986 abrexdom 35625 diaf11N 38800 dibf11N 38912 gneispace3 41420 fresfo 44214 funbrafvb 44320 funopafvb 44321 funbrafv22b 44414 funopafv2b 44415 |
Copyright terms: Public domain | W3C validator |