Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > funmpt | Structured version Visualization version GIF version |
Description: A function in maps-to notation is a function. (Contributed by Mario Carneiro, 13-Jan-2013.) |
Ref | Expression |
---|---|
funmpt | ⊢ Fun (𝑥 ∈ 𝐴 ↦ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | funopab4 6417 | . 2 ⊢ Fun {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} | |
2 | df-mpt 5136 | . . 3 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} | |
3 | 2 | funeqi 6401 | . 2 ⊢ (Fun (𝑥 ∈ 𝐴 ↦ 𝐵) ↔ Fun {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}) |
4 | 1, 3 | mpbir 234 | 1 ⊢ Fun (𝑥 ∈ 𝐴 ↦ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 399 = wceq 1543 ∈ wcel 2110 {copab 5115 ↦ cmpt 5135 Fun wfun 6374 |
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-8 2112 ax-9 2120 ax-10 2141 ax-11 2158 ax-12 2175 ax-ext 2708 ax-sep 5192 ax-nul 5199 ax-pr 5322 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2071 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2886 df-ral 3066 df-rab 3070 df-v 3410 df-dif 3869 df-un 3871 df-in 3873 df-ss 3883 df-nul 4238 df-if 4440 df-sn 4542 df-pr 4544 df-op 4548 df-br 5054 df-opab 5116 df-mpt 5136 df-id 5455 df-xp 5557 df-rel 5558 df-cnv 5559 df-co 5560 df-fun 6382 |
This theorem is referenced by: funmpt2 6419 resfunexg 7031 mptexg 7037 mptexgf 7038 mptexw 7726 brtpos2 7974 tposfun 7984 mptfi 8975 sniffsupp 9016 cantnfrescl 9291 cantnflem1 9304 r0weon 9626 axcc2lem 10050 mptct 10152 negfi 11781 mptnn0fsupp 13570 ccatalpha 14150 mreacs 17161 acsfn 17162 isofval 17262 lubfun 17858 glbfun 17871 acsficl2d 18058 gsum2dlem2 19356 gsum2d 19357 dprdfinv 19406 dprdfadd 19407 dmdprdsplitlem 19424 dpjidcl 19445 mptscmfsupp0 19964 pjpm 20670 frlmphllem 20742 frlmphl 20743 uvcff 20753 uvcresum 20755 psrass1lemOLD 20899 psrass1lem 20902 psrlidm 20928 psrridm 20929 psrass1 20930 psrass23l 20933 psrcom 20934 psrass23 20935 mplsubrg 20967 mplmon 20992 mplmonmul 20993 mplcoe1 20994 mplcoe5 20997 mplbas2 20999 evlslem2 21039 evlslem6 21041 psropprmul 21159 coe1mul2 21190 oftpos 21349 pmatcollpw2lem 21674 tgrest 22056 cmpfi 22305 1stcrestlem 22349 ptcnplem 22518 xkoinjcn 22584 symgtgp 23003 eltsms 23030 rrxmval 24302 tdeglem4 24957 tdeglem4OLD 24958 plypf1 25106 tayl0 25254 taylthlem1 25265 xrlimcnp 25851 abrexexd 30573 ofpreima 30722 mptctf 30772 gsummptres2 31032 psgnfzto1stlem 31086 rmfsupp2 31211 elrspunidl 31320 locfinreflem 31504 measdivcstALTV 31905 sxbrsigalem0 31950 sitgf 32026 nosupno 33643 noinfno 33658 imageval 33969 poimirlem30 35544 poimir 35547 evlsbagval 39985 mhphf 39995 choicefi 42413 fourierdlem80 43402 sge0tsms 43593 scmsuppss 45381 rmfsupp 45383 scmfsupp 45387 fdivval 45558 |
Copyright terms: Public domain | W3C validator |