Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > funmpt2 | Structured version Visualization version GIF version |
Description: Functionality of a class given by a maps-to notation. (Contributed by FL, 17-Feb-2008.) (Revised by Mario Carneiro, 31-May-2014.) |
Ref | Expression |
---|---|
funmpt2.1 | ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) |
Ref | Expression |
---|---|
funmpt2 | ⊢ Fun 𝐹 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | funmpt 6469 | . 2 ⊢ Fun (𝑥 ∈ 𝐴 ↦ 𝐵) | |
2 | funmpt2.1 | . . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) | |
3 | 2 | funeqi 6452 | . 2 ⊢ (Fun 𝐹 ↔ Fun (𝑥 ∈ 𝐴 ↦ 𝐵)) |
4 | 1, 3 | mpbir 230 | 1 ⊢ Fun 𝐹 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1542 ↦ cmpt 5162 Fun wfun 6425 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2015 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2158 ax-12 2175 ax-ext 2711 ax-sep 5227 ax-nul 5234 ax-pr 5356 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3an 1088 df-tru 1545 df-fal 1555 df-ex 1787 df-nf 1791 df-sb 2072 df-mo 2542 df-eu 2571 df-clab 2718 df-cleq 2732 df-clel 2818 df-nfc 2891 df-ral 3071 df-rab 3075 df-v 3433 df-dif 3895 df-un 3897 df-in 3899 df-ss 3909 df-nul 4263 df-if 4466 df-sn 4568 df-pr 4570 df-op 4574 df-br 5080 df-opab 5142 df-mpt 5163 df-id 5489 df-xp 5595 df-rel 5596 df-cnv 5597 df-co 5598 df-fun 6433 |
This theorem is referenced by: pwfilem 8940 cantnfp1lem1 9412 tz9.12lem2 9545 tz9.12lem3 9546 rankf 9551 djuun 9683 cardf2 9700 fin23lem30 10097 hashf1rn 14063 oppccatf 17435 funtopon 22065 qustgpopn 23267 ustn0 23368 metuval 23701 cphsscph 24411 ipasslem8 29193 xppreima2 30982 funcnvmpt 30998 fsuppcurry1 31054 fsuppcurry2 31055 gsummpt2co 31302 zarclsint 31816 zartopn 31819 zarmxt1 31824 zarcmplem 31825 metidval 31834 pstmval 31839 brsiga 32145 measbasedom 32164 sseqval 32349 ballotlem7 32496 sinccvglem 33624 bj-evalfun 35238 bj-ccinftydisj 35378 bj-elccinfty 35379 bj-minftyccb 35390 iscard4 41117 harval3 41120 comptiunov2i 41282 icccncfext 43397 stoweidlem27 43537 stirlinglem14 43597 fourierdlem70 43686 fourierdlem71 43687 hoi2toco 44114 mptcfsupp 45683 lcoc0 45730 lincresunit2 45786 |
Copyright terms: Public domain | W3C validator |