| 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 6530 | . 2 ⊢ Fun {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} | |
| 2 | df-mpt 5181 | . . 3 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} | |
| 3 | 2 | funeqi 6514 | . 2 ⊢ (Fun (𝑥 ∈ 𝐴 ↦ 𝐵) ↔ Fun {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}) |
| 4 | 1, 3 | mpbir 231 | 1 ⊢ Fun (𝑥 ∈ 𝐴 ↦ 𝐵) |
| Colors of variables: wff setvar class |
| Syntax hints: ∧ wa 395 = wceq 1542 ∈ wcel 2114 {copab 5161 ↦ cmpt 5180 Fun wfun 6487 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-sep 5242 ax-nul 5252 ax-pr 5378 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ral 3053 df-rex 3062 df-rab 3401 df-v 3443 df-dif 3905 df-un 3907 df-ss 3919 df-nul 4287 df-if 4481 df-sn 4582 df-pr 4584 df-op 4588 df-br 5100 df-opab 5162 df-mpt 5181 df-id 5520 df-xp 5631 df-rel 5632 df-cnv 5633 df-co 5634 df-fun 6495 |
| This theorem is referenced by: funmpt2 6532 resfunexg 7163 mptexg 7169 mptexgf 7170 mptexw 7899 brtpos2 8176 tposfun 8186 mptfi 9255 fsuppssov1 9291 sniffsupp 9307 cantnfrescl 9589 cantnflem1 9602 r0weon 9926 axcc2lem 10350 mptct 10452 negfi 12095 mptnn0fsupp 13924 ccatalpha 14521 mreacs 17585 acsfn 17586 isofval 17685 lubfun 18277 glbfun 18290 acsficl2d 18479 gsum2dlem2 19904 gsum2d 19905 dprdfinv 19954 dprdfadd 19955 dmdprdsplitlem 19972 dpjidcl 19993 mptscmfsupp0 20882 pjpm 21667 frlmphllem 21739 uvcff 21750 uvcresum 21752 psrass1lem 21892 psrlidm 21921 psrridm 21922 psrass1 21923 psrass23l 21926 psrcom 21927 psrass23 21928 mplsubrg 21964 mplmon 21994 mplmonmul 21995 mplcoe1 21996 mplcoe5 21999 mplbas2 22001 evlslem2 22038 evlslem6 22040 evlsvvvallem2 22051 evlsvvval 22052 psdmplcl 22109 psdmul 22113 psropprmul 22182 coe1mul2 22215 evls1fpws 22317 oftpos 22400 pmatcollpw2lem 22725 tgrest 23107 cmpfi 23356 1stcrestlem 23400 ptcnplem 23569 xkoinjcn 23635 symgtgp 24054 eltsms 24081 rrxmval 25365 tdeglem4 26025 plypf1 26177 tayl0 26329 taylthlem1 26341 xrlimcnp 26938 nosupno 27675 noinfno 27690 abrexexd 32566 ofpreima 32725 fisuppov1 32743 mptiffisupp 32753 mptctf 32776 gsummptres2 33117 psgnfzto1stlem 33163 rmfsupp2 33301 elrspunidl 33490 elrspunsn 33491 locfinreflem 33978 measdivcstALTV 34363 sitgf 34485 imageval 36103 poimirlem30 37822 poimir 37825 selvvvval 42864 evlselv 42866 mhphf 42876 choicefi 45480 rn1st 45553 fourierdlem80 46466 sge0tsms 46660 scmsuppss 48653 rmfsupp 48655 scmfsupp 48657 fdivval 48821 |
| Copyright terms: Public domain | W3C validator |