![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fvconst2 | Structured version Visualization version GIF version |
Description: The value of a constant function. (Contributed by NM, 16-Apr-2005.) |
Ref | Expression |
---|---|
fvconst2.1 | ⊢ 𝐵 ∈ V |
Ref | Expression |
---|---|
fvconst2 | ⊢ (𝐶 ∈ 𝐴 → ((𝐴 × {𝐵})‘𝐶) = 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fvconst2.1 | . 2 ⊢ 𝐵 ∈ V | |
2 | fvconst2g 7198 | . 2 ⊢ ((𝐵 ∈ V ∧ 𝐶 ∈ 𝐴) → ((𝐴 × {𝐵})‘𝐶) = 𝐵) | |
3 | 1, 2 | mpan 689 | 1 ⊢ (𝐶 ∈ 𝐴 → ((𝐴 × {𝐵})‘𝐶) = 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1542 ∈ wcel 2107 Vcvv 3475 {csn 4627 × cxp 5673 ‘cfv 6540 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-sep 5298 ax-nul 5305 ax-pr 5426 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-ral 3063 df-rex 3072 df-rab 3434 df-v 3477 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4322 df-if 4528 df-sn 4628 df-pr 4630 df-op 4634 df-uni 4908 df-br 5148 df-opab 5210 df-mpt 5231 df-id 5573 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-iota 6492 df-fun 6542 df-fn 6543 df-f 6544 df-fv 6548 |
This theorem is referenced by: ovconst2 7582 mapsncnv 8883 ofsubeq0 12205 ofsubge0 12207 ser0f 14017 hashinf 14291 iserge0 15603 iseraltlem1 15624 sum0 15663 sumz 15664 harmonic 15801 prodf1f 15834 fprodntriv 15882 prod1 15884 setcmon 18033 0mhm 18696 mulgfval 18946 mulgpropd 18990 dprdsubg 19886 pwspjmhmmgpd 20131 0lmhm 20639 frlmlmod 21288 frlmlss 21290 frlmbas 21294 frlmip 21317 islindf4 21377 mplsubglem 21540 coe1tm 21777 mdetuni0 22105 txkgen 23138 xkofvcn 23170 nmo0 24234 pcorevlem 24524 rrxip 24889 mbfpos 25150 0pval 25170 0pledm 25172 xrge0f 25231 itg2ge0 25235 ibl0 25286 bddibl 25339 dvcmul 25443 dvef 25479 rolle 25489 dveq0 25499 dv11cn 25500 ftc2 25543 tdeglem4 25559 tdeglem4OLD 25560 ply1rem 25663 fta1g 25667 fta1blem 25668 0dgrb 25742 dgrnznn 25743 dgrlt 25762 plymul0or 25776 plydivlem4 25791 plyrem 25800 fta1 25803 vieta1lem2 25806 elqaalem3 25816 aaliou2 25835 ulmdvlem1 25894 dchrelbas2 26720 dchrisumlem3 26974 noetasuplem4 27219 noetainflem4 27223 axlowdimlem9 28188 axlowdimlem12 28191 axlowdimlem17 28196 0oval 30019 occllem 30534 ho01i 31059 0cnfn 31211 0lnfn 31216 nmfn0 31218 nlelchi 31292 opsqrlem2 31372 opsqrlem4 31374 opsqrlem5 31375 hmopidmchi 31382 elrspunidl 32504 lbsdiflsp0 32656 evls1maprnss 32705 breprexpnat 33584 circlemethnat 33591 circlevma 33592 connpconn 34164 txsconnlem 34169 cvxsconn 34172 cvmliftphtlem 34246 fullfunfv 34857 matunitlindflem1 36422 matunitlindflem2 36423 ptrecube 36426 poimirlem1 36427 poimirlem2 36428 poimirlem3 36429 poimirlem4 36430 poimirlem5 36431 poimirlem6 36432 poimirlem7 36433 poimirlem10 36436 poimirlem11 36437 poimirlem12 36438 poimirlem16 36442 poimirlem17 36443 poimirlem19 36445 poimirlem20 36446 poimirlem22 36448 poimirlem23 36449 poimirlem28 36454 poimirlem29 36455 poimirlem30 36456 poimirlem31 36457 poimirlem32 36458 poimir 36459 broucube 36460 mblfinlem2 36464 itg2addnclem 36477 itg2addnc 36480 ftc1anclem5 36503 ftc2nc 36508 cnpwstotbnd 36603 lfl0f 37877 eqlkr2 37908 lcd0vvalN 40422 frlm0vald 41059 evlsvvval 41085 selvvvval 41107 evlselv 41109 mzpsubst 41419 mzpcompact2lem 41422 mzpcong 41644 hbtlem2 41799 mncn0 41814 mpaaeu 41825 aaitgo 41837 rngunsnply 41848 cantnfresb 42007 hashnzfzclim 43014 ofsubid 43016 dvconstbi 43026 binomcxplemnotnn0 43048 n0p 43663 snelmap 43704 fvconst0ci 47427 fvconstdomi 47428 aacllem 47750 |
Copyright terms: Public domain | W3C validator |