![]() |
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 2752 | . . 3 ⊢ dom 𝐴 = dom 𝐴 | |
2 | 1 | biantru 527 | . 2 ⊢ (Fun 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴)) |
3 | df-fn 6044 | . 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 1624 dom cdm 5258 Fun wfun 6035 Fn wfn 6036 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1863 ax-4 1878 ax-5 1980 ax-6 2046 ax-7 2082 ax-9 2140 ax-ext 2732 |
This theorem depends on definitions: df-bi 197 df-an 385 df-ex 1846 df-cleq 2745 df-fn 6044 |
This theorem is referenced by: funfnd 6072 funssxp 6214 funforn 6275 funbrfvb 6391 funopfvb 6392 ssimaex 6417 fvco 6428 fvco4i 6430 eqfunfv 6471 fvimacnvi 6486 unpreima 6496 respreima 6499 elrnrexdm 6518 elrnrexdmb 6519 ffvresb 6549 funiun 6567 funressn 6581 funresdfunsn 6611 resfunexg 6635 funex 6638 funiunfv 6661 elunirn 6664 suppval1 7461 funsssuppss 7482 wfrlem4 7579 smores 7610 smores2 7612 tfrlem1 7633 rdgsucg 7680 rdglimg 7682 fundmfibi 8402 resfnfinfin 8403 residfi 8404 mptfi 8422 resfifsupp 8460 ordtypelem4 8583 ordtypelem6 8585 ordtypelem7 8586 ordtypelem9 8588 ordtypelem10 8589 harwdom 8652 ackbij2 9249 brdom3 9534 brdom5 9535 brdom4 9536 mptct 9544 smobeth 9592 fpwwe2lem11 9646 hashkf 13305 hashfun 13408 hashimarn 13411 resunimafz0 13413 fclim 14475 isstruct2 16061 xpsc0 16414 xpsc1 16415 invf 16621 coapm 16914 psgnghm 20120 lindfrn 20354 ofco2 20451 dfac14 21615 perfdvf 23858 c1lip2 23952 taylf 24306 lpvtx 26154 upgrle2 26191 uhgrvtxedgiedgb 26222 ausgrumgri 26253 uhgr2edg 26291 ushgredgedg 26312 ushgredgedgloop 26314 subgruhgredgd 26367 subuhgr 26369 subupgr 26370 subumgr 26371 subusgr 26372 dfnbgr3 26422 vtxdun 26579 upgrewlkle2 26704 wlkiswwlks1 26968 vdn0conngrumgrv2 27340 eupthvdres 27379 hlimf 28395 adj1o 29054 abrexdomjm 29644 iunpreima 29682 fresf1o 29734 unipreima 29747 xppreima 29750 mptctf 29796 sitgf 30710 orvcval2 30821 frrlem4 32081 elno3 32106 noextenddif 32119 noextendlt 32120 noextendgt 32121 nosupbnd2lem1 32159 noetalem3 32163 fullfunfnv 32351 fullfunfv 32352 abrexdom 33830 diaf11N 36832 dibf11N 36944 gneispace3 38925 gneispace 38926 gneispacef2 38928 funcoressn 41705 funbrafvb 41734 funopafvb 41735 |
Copyright terms: Public domain | W3C validator |