![]() |
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 2795 | . . 3 ⊢ dom 𝐴 = dom 𝐴 | |
2 | 1 | biantru 530 | . 2 ⊢ (Fun 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴)) |
3 | df-fn 6228 | . 2 ⊢ (𝐴 Fn dom 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴)) | |
4 | 2, 3 | bitr4i 279 | 1 ⊢ (Fun 𝐴 ↔ 𝐴 Fn dom 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 207 ∧ wa 396 = wceq 1522 dom cdm 5443 Fun wfun 6219 Fn wfn 6220 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-9 2091 ax-ext 2769 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1762 df-cleq 2788 df-fn 6228 |
This theorem is referenced by: funfnd 6256 funssxp 6403 funforn 6465 funbrfvb 6588 funopfvb 6589 ssimaex 6615 fvco 6626 fvco4i 6629 eqfunfv 6672 fvimacnvi 6687 unpreima 6698 respreima 6701 elrnrexdm 6720 elrnrexdmb 6721 ffvresb 6751 funiun 6772 funressn 6784 funresdfunsn 6818 funex 6848 elunirn 6875 suppval1 7687 funsssuppss 7707 wfrlem4OLD 7810 smores 7841 rdgsucg 7911 rdglimg 7913 fundmfibi 8649 residfi 8651 mptfi 8669 ordtypelem6 8833 ordtypelem7 8834 harwdom 8900 ackbij2 9511 mptct 9806 smobeth 9854 hashkf 13542 hashfun 13646 fclim 14744 coapm 17160 psgnghm 20406 lindfrn 20647 ausgrumgri 26635 dfnbgr3 26803 wlkiswwlks1 27332 vdn0conngrumgrv2 27662 hlimf 28705 adj1o 29362 abrexdomjm 29959 iunpreima 30006 fresf1o 30066 unipreima 30081 xppreima 30084 mptctf 30141 orvcval2 31333 elno3 32772 noextenddif 32785 noextendlt 32786 noextendgt 32787 nosupbnd2lem1 32825 noetalem3 32829 fullfunfnv 33017 fullfunfv 33018 abrexdom 34556 diaf11N 37735 dibf11N 37847 gneispace3 39987 funbrafvb 42891 funopafvb 42892 funbrafv22b 42985 funopafv2b 42986 |
Copyright terms: Public domain | W3C validator |