| 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 7222 | . 2 ⊢ ((𝐵 ∈ V ∧ 𝐶 ∈ 𝐴) → ((𝐴 × {𝐵})‘𝐶) = 𝐵) | |
| 3 | 1, 2 | mpan 690 | 1 ⊢ (𝐶 ∈ 𝐴 → ((𝐴 × {𝐵})‘𝐶) = 𝐵) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 = wceq 1540 ∈ wcel 2108 Vcvv 3480 {csn 4626 × cxp 5683 ‘cfv 6561 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-sep 5296 ax-nul 5306 ax-pr 5432 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ne 2941 df-ral 3062 df-rex 3071 df-rab 3437 df-v 3482 df-dif 3954 df-un 3956 df-ss 3968 df-nul 4334 df-if 4526 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-br 5144 df-opab 5206 df-mpt 5226 df-id 5578 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-rn 5696 df-iota 6514 df-fun 6563 df-fn 6564 df-f 6565 df-fv 6569 |
| This theorem is referenced by: ovconst2 7613 mapsncnv 8933 ofsubeq0 12263 ofsubge0 12265 ser0f 14096 hashinf 14374 iserge0 15697 iseraltlem1 15718 sum0 15757 sumz 15758 harmonic 15895 prodf1f 15928 fprodntriv 15978 prod1 15980 setcmon 18132 0mhm 18832 mulgfval 19087 mulgpropd 19134 dprdsubg 20044 pwspjmhmmgpd 20325 0lmhm 21039 frlmlmod 21769 frlmlss 21771 frlmbas 21775 frlmip 21798 islindf4 21858 mplsubglem 22019 psdmvr 22173 coe1tm 22276 evls1maprnss 22382 mdetuni0 22627 txkgen 23660 xkofvcn 23692 nmo0 24756 pcorevlem 25059 rrxip 25424 mbfpos 25686 0pval 25706 0pledm 25708 xrge0f 25766 itg2ge0 25770 ibl0 25822 bddibl 25875 dvcmul 25981 dvef 26018 rolle 26028 dveq0 26039 dv11cn 26040 ftc2 26085 tdeglem4 26099 ply1rem 26205 fta1g 26209 fta1blem 26210 0dgrb 26285 dgrnznn 26286 dgrlt 26306 plymul0or 26322 plydivlem4 26338 plyrem 26347 fta1 26350 vieta1lem2 26353 elqaalem3 26363 aaliou2 26382 ulmdvlem1 26443 dchrelbas2 27281 dchrisumlem3 27535 noetasuplem4 27781 noetainflem4 27785 axlowdimlem9 28965 axlowdimlem12 28968 axlowdimlem17 28973 0oval 30807 occllem 31322 ho01i 31847 0cnfn 31999 0lnfn 32004 nmfn0 32006 nlelchi 32080 opsqrlem2 32160 opsqrlem4 32162 opsqrlem5 32163 hmopidmchi 32170 elrspunidl 33456 coe1zfv 33612 lbsdiflsp0 33677 breprexpnat 34649 circlemethnat 34656 circlevma 34657 connpconn 35240 txsconnlem 35245 cvxsconn 35248 cvmliftphtlem 35322 fullfunfv 35948 matunitlindflem1 37623 matunitlindflem2 37624 ptrecube 37627 poimirlem1 37628 poimirlem2 37629 poimirlem3 37630 poimirlem4 37631 poimirlem5 37632 poimirlem6 37633 poimirlem7 37634 poimirlem10 37637 poimirlem11 37638 poimirlem12 37639 poimirlem16 37643 poimirlem17 37644 poimirlem19 37646 poimirlem20 37647 poimirlem22 37649 poimirlem23 37650 poimirlem28 37655 poimirlem29 37656 poimirlem30 37657 poimirlem31 37658 poimirlem32 37659 poimir 37660 broucube 37661 mblfinlem2 37665 itg2addnclem 37678 itg2addnc 37681 ftc1anclem5 37704 ftc2nc 37709 cnpwstotbnd 37804 lfl0f 39070 eqlkr2 39101 lcd0vvalN 41615 frlm0vald 42549 evlsvvval 42573 selvvvval 42595 evlselv 42597 mzpsubst 42759 mzpcompact2lem 42762 mzpcong 42984 hbtlem2 43136 mncn0 43151 mpaaeu 43162 aaitgo 43174 rngunsnply 43181 cantnfresb 43337 hashnzfzclim 44341 ofsubid 44343 dvconstbi 44353 binomcxplemnotnn0 44375 n0p 45050 snelmap 45087 fvconst0ci 48790 fvconstdomi 48791 aacllem 49320 |
| Copyright terms: Public domain | W3C validator |