![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fvconst2g | Structured version Visualization version GIF version |
Description: The value of a constant function. (Contributed by NM, 20-Aug-2005.) |
Ref | Expression |
---|---|
fvconst2g | ⊢ ((𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐴) → ((𝐴 × {𝐵})‘𝐶) = 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fconstg 6768 | . 2 ⊢ (𝐵 ∈ 𝐷 → (𝐴 × {𝐵}):𝐴⟶{𝐵}) | |
2 | fvconst 7154 | . 2 ⊢ (((𝐴 × {𝐵}):𝐴⟶{𝐵} ∧ 𝐶 ∈ 𝐴) → ((𝐴 × {𝐵})‘𝐶) = 𝐵) | |
3 | 1, 2 | sylan 579 | 1 ⊢ ((𝐵 ∈ 𝐷 ∧ 𝐶 ∈ 𝐴) → ((𝐴 × {𝐵})‘𝐶) = 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 = wceq 1533 ∈ wcel 2098 {csn 4620 × cxp 5664 ⟶wf 6529 ‘cfv 6533 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2163 ax-ext 2695 ax-sep 5289 ax-nul 5296 ax-pr 5417 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2526 df-eu 2555 df-clab 2702 df-cleq 2716 df-clel 2802 df-nfc 2877 df-ne 2933 df-ral 3054 df-rex 3063 df-rab 3425 df-v 3468 df-dif 3943 df-un 3945 df-in 3947 df-ss 3957 df-nul 4315 df-if 4521 df-sn 4621 df-pr 4623 df-op 4627 df-uni 4900 df-br 5139 df-opab 5201 df-mpt 5222 df-id 5564 df-xp 5672 df-rel 5673 df-cnv 5674 df-co 5675 df-dm 5676 df-rn 5677 df-iota 6485 df-fun 6535 df-fn 6536 df-f 6537 df-fv 6541 |
This theorem is referenced by: fconst2g 7196 fvconst2 7197 ofc1 7689 ofc2 7690 caofid0l 7694 caofid0r 7695 caofid1 7696 caofid2 7697 fnsuppres 8170 ser0 14016 ser1const 14020 exp1 14029 expp1 14030 climconst2 15488 climaddc1 15575 climmulc2 15577 climsubc1 15578 climsubc2 15579 climlec2 15601 fsumconst 15732 supcvg 15798 prodf1 15833 prod0 15883 fprodconst 15918 seq1st 16504 algr0 16505 algrf 16506 ramz 16954 pwsbas 17429 pwsplusgval 17432 pwsmulrval 17433 pwsle 17434 pwsvscafval 17436 pwspjmhm 18742 pwsco1mhm 18744 pwsinvg 18968 mulgnngsum 18991 mulg1 18993 mulgnnp1 18994 mulgnnsubcl 18998 mulgnn0z 19013 mulgnndir 19015 mulgnn0di 19730 gsumconst 19839 pwslmod 20802 frlmvscaval 21623 psrlidm 21824 coe1tm 22105 coe1fzgsumd 22136 evl1scad 22164 decpmatid 22582 pmatcollpwscmatlem1 22601 lmconst 23075 cnconst2 23097 xkoptsub 23468 xkopt 23469 xkopjcn 23470 tmdgsum 23909 tmdgsum2 23910 symgtgp 23920 cstucnd 24099 pcoptcl 24858 pcopt 24859 pcopt2 24860 dvidlem 25754 dvconst 25756 dvnff 25763 dvn0 25764 dvcmul 25785 dvcmulf 25786 fta1blem 26014 plyeq0lem 26052 coemulc 26097 dgreq0 26108 dgrmulc 26114 qaa 26165 dchrisumlema 27325 suppovss 32330 fdifsuppconst 32335 evls1scafv 33074 ofcc 33559 ofcof 33560 sseqf 33846 sseqp1 33849 lpadleft 34150 cvmlift3lem9 34773 ismrer1 37162 frlmvscadiccat 41539 evlsscaval 41591 fsuppssind 41620 ofoafo 42561 ofoaid1 42563 ofoaid2 42564 naddcnffo 42569 naddcnfid1 42572 dvsinax 45080 stoweidlem21 45188 stoweidlem47 45214 elaa2 45401 zlmodzxzscm 47188 2sphere0 47590 fvconstr 47676 fvconstrn0 47677 |
Copyright terms: Public domain | W3C validator |