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 6956 | . 2 ⊢ ((𝐵 ∈ V ∧ 𝐶 ∈ 𝐴) → ((𝐴 × {𝐵})‘𝐶) = 𝐵) | |
3 | 1, 2 | mpan 686 | 1 ⊢ (𝐶 ∈ 𝐴 → ((𝐴 × {𝐵})‘𝐶) = 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1528 ∈ wcel 2105 Vcvv 3492 {csn 4557 × cxp 5546 ‘cfv 6348 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 ax-sep 5194 ax-nul 5201 ax-pr 5320 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-mo 2615 df-eu 2647 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-ne 3014 df-ral 3140 df-rex 3141 df-rab 3144 df-v 3494 df-sbc 3770 df-dif 3936 df-un 3938 df-in 3940 df-ss 3949 df-nul 4289 df-if 4464 df-sn 4558 df-pr 4560 df-op 4564 df-uni 4831 df-br 5058 df-opab 5120 df-mpt 5138 df-id 5453 df-xp 5554 df-rel 5555 df-cnv 5556 df-co 5557 df-dm 5558 df-rn 5559 df-iota 6307 df-fun 6350 df-fn 6351 df-f 6352 df-fv 6356 |
This theorem is referenced by: ovconst2 7317 mapsncnv 8445 ofsubeq0 11623 ofsubge0 11625 ser0f 13411 hashinf 13683 iserge0 15005 iseraltlem1 15026 sum0 15066 sumz 15067 harmonic 15202 prodf1f 15236 fprodntriv 15284 prod1 15286 setcmon 17335 0mhm 17972 mulgfval 18164 mulgpropd 18207 dprdsubg 19075 0lmhm 19741 mplsubglem 20142 coe1tm 20369 frlmlmod 20821 frlmlss 20823 frlmbas 20827 frlmip 20850 islindf4 20910 mdetuni0 21158 txkgen 22188 xkofvcn 22220 nmo0 23271 pcorevlem 23557 rrxip 23920 mbfpos 24179 0pval 24199 0pledm 24201 xrge0f 24259 itg2ge0 24263 ibl0 24314 bddibl 24367 dvcmul 24468 dvef 24504 rolle 24514 dveq0 24524 dv11cn 24525 ftc2 24568 tdeglem4 24581 ply1rem 24684 fta1g 24688 fta1blem 24689 0dgrb 24763 dgrnznn 24764 dgrlt 24783 plymul0or 24797 plydivlem4 24812 plyrem 24821 fta1 24824 vieta1lem2 24827 elqaalem3 24837 aaliou2 24856 ulmdvlem1 24915 dchrelbas2 25740 dchrisumlem3 25994 axlowdimlem9 26663 axlowdimlem12 26666 axlowdimlem17 26671 0oval 28492 occllem 29007 ho01i 29532 0cnfn 29684 0lnfn 29689 nmfn0 29691 nlelchi 29765 opsqrlem2 29845 opsqrlem4 29847 opsqrlem5 29848 hmopidmchi 29855 lbsdiflsp0 30921 breprexpnat 31804 circlemethnat 31811 circlevma 31812 connpconn 32379 txsconnlem 32384 cvxsconn 32387 cvmliftphtlem 32461 noetalem3 33116 fullfunfv 33305 matunitlindflem1 34769 matunitlindflem2 34770 ptrecube 34773 poimirlem1 34774 poimirlem2 34775 poimirlem3 34776 poimirlem4 34777 poimirlem5 34778 poimirlem6 34779 poimirlem7 34780 poimirlem10 34783 poimirlem11 34784 poimirlem12 34785 poimirlem16 34789 poimirlem17 34790 poimirlem19 34792 poimirlem20 34793 poimirlem22 34795 poimirlem23 34796 poimirlem28 34801 poimirlem29 34802 poimirlem30 34803 poimirlem31 34804 poimirlem32 34805 poimir 34806 broucube 34807 mblfinlem2 34811 itg2addnclem 34824 itg2addnc 34827 ftc1anclem5 34852 ftc2nc 34857 cnpwstotbnd 34956 lfl0f 36085 eqlkr2 36116 lcd0vvalN 38629 uvcn0 39029 mzpsubst 39223 mzpcompact2lem 39226 mzpcong 39447 hbtlem2 39602 mncn0 39617 mpaaeu 39628 aaitgo 39640 rngunsnply 39651 hashnzfzclim 40531 ofsubid 40533 dvconstbi 40543 binomcxplemnotnn0 40565 n0p 41182 snelmap 41223 aacllem 44830 |
Copyright terms: Public domain | W3C validator |