![]() |
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 6535 | . 2 ⊢ Fun {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} | |
2 | df-mpt 5187 | . . 3 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} | |
3 | 2 | funeqi 6519 | . 2 ⊢ (Fun (𝑥 ∈ 𝐴 ↦ 𝐵) ↔ Fun {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}) |
4 | 1, 3 | mpbir 230 | 1 ⊢ Fun (𝑥 ∈ 𝐴 ↦ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 396 = wceq 1541 ∈ wcel 2106 {copab 5165 ↦ cmpt 5186 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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2707 ax-sep 5254 ax-nul 5261 ax-pr 5382 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2887 df-ral 3063 df-rex 3072 df-rab 3406 df-v 3445 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-nul 4281 df-if 4485 df-sn 4585 df-pr 4587 df-op 4591 df-br 5104 df-opab 5166 df-mpt 5187 df-id 5529 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-fun 6495 |
This theorem is referenced by: funmpt2 6537 resfunexg 7161 mptexg 7167 mptexgf 7168 mptexw 7881 brtpos2 8159 tposfun 8169 mptfi 9291 sniffsupp 9332 cantnfrescl 9608 cantnflem1 9621 r0weon 9944 axcc2lem 10368 mptct 10470 negfi 12100 mptnn0fsupp 13894 ccatalpha 14473 mreacs 17530 acsfn 17531 isofval 17632 lubfun 18233 glbfun 18246 acsficl2d 18433 gsum2dlem2 19739 gsum2d 19740 dprdfinv 19789 dprdfadd 19790 dmdprdsplitlem 19807 dpjidcl 19828 mptscmfsupp0 20372 pjpm 21099 frlmphllem 21171 frlmphl 21172 uvcff 21182 uvcresum 21184 psrass1lemOLD 21327 psrass1lem 21330 psrlidm 21356 psrridm 21357 psrass1 21358 psrass23l 21361 psrcom 21362 psrass23 21363 mplsubrg 21395 mplmon 21420 mplmonmul 21421 mplcoe1 21422 mplcoe5 21425 mplbas2 21427 evlslem2 21473 evlslem6 21475 psropprmul 21593 coe1mul2 21624 oftpos 21785 pmatcollpw2lem 22110 tgrest 22494 cmpfi 22743 1stcrestlem 22787 ptcnplem 22956 xkoinjcn 23022 symgtgp 23441 eltsms 23468 rrxmval 24753 tdeglem4 25408 tdeglem4OLD 25409 plypf1 25557 tayl0 25705 taylthlem1 25716 xrlimcnp 26302 nosupno 27035 noinfno 27050 abrexexd 31321 ofpreima 31467 mptctf 31517 gsummptres2 31778 psgnfzto1stlem 31832 rmfsupp2 31958 elrspunidl 32082 evls1fpws 32149 locfinreflem 32290 measdivcstALTV 32693 sitgf 32816 imageval 34482 poimirlem30 36075 poimir 36078 evlsbagval 40699 mhphf 40709 choicefi 43357 rn1st 43439 fourierdlem80 44359 sge0tsms 44553 scmsuppss 46380 rmfsupp 46382 scmfsupp 46386 fdivval 46557 |
Copyright terms: Public domain | W3C validator |