Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > fnconstg | Structured version Visualization version GIF version |
Description: A Cartesian product with a singleton is a constant function. (Contributed by NM, 24-Jul-2014.) |
Ref | Expression |
---|---|
fnconstg | ⊢ (𝐵 ∈ 𝑉 → (𝐴 × {𝐵}) Fn 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fconstg 6560 | . 2 ⊢ (𝐵 ∈ 𝑉 → (𝐴 × {𝐵}):𝐴⟶{𝐵}) | |
2 | 1 | ffnd 6509 | 1 ⊢ (𝐵 ∈ 𝑉 → (𝐴 × {𝐵}) Fn 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2110 {csn 4560 × cxp 5547 Fn wfn 6344 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 ax-sep 5195 ax-nul 5202 ax-pr 5321 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-mo 2618 df-eu 2650 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-ral 3143 df-rab 3147 df-v 3496 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-nul 4291 df-if 4467 df-sn 4561 df-pr 4563 df-op 4567 df-br 5059 df-opab 5121 df-mpt 5139 df-id 5454 df-xp 5555 df-rel 5556 df-cnv 5557 df-co 5558 df-dm 5559 df-rn 5560 df-fun 6351 df-fn 6352 df-f 6353 |
This theorem is referenced by: fconst2g 6959 ofc1 7426 ofc2 7427 caofid0l 7431 caofid0r 7432 caofid1 7433 caofid2 7434 fnsuppres 7851 fczsupp0 7853 fczfsuppd 8845 brwdom2 9031 cantnf0 9132 ofnegsub 11630 ofsubge0 11631 pwsplusgval 16757 pwsmulrval 16758 pwsvscafval 16761 pwsco1mhm 17990 dprdsubg 19140 pwsmgp 19362 pwssplit1 19825 frlmpwsfi 20890 frlmbas 20893 frlmvscaval 20906 islindf4 20976 tmdgsum2 22698 0plef 24267 0pledm 24268 itg1ge0 24281 mbfi1fseqlem5 24314 xrge0f 24326 itg2ge0 24330 itg2addlem 24353 bddibl 24434 dvidlem 24507 rolle 24581 dveq0 24591 dv11cn 24592 tdeglem4 24648 mdeg0 24658 fta1blem 24756 qaa 24906 basellem9 25660 ofcc 31360 ofcof 31361 eulerpartlemt 31624 noextendseq 33169 matunitlindflem1 34882 matunitlindflem2 34883 ptrecube 34886 poimirlem1 34887 poimirlem2 34888 poimirlem3 34889 poimirlem4 34890 poimirlem5 34891 poimirlem6 34892 poimirlem7 34893 poimirlem10 34896 poimirlem11 34897 poimirlem12 34898 poimirlem16 34902 poimirlem17 34903 poimirlem19 34905 poimirlem20 34906 poimirlem22 34908 poimirlem23 34909 poimirlem28 34914 poimirlem29 34915 poimirlem31 34917 poimirlem32 34918 broucube 34920 cnpwstotbnd 35069 eqlkr2 36230 pwssplit4 39682 mpaaeu 39743 rngunsnply 39766 ofdivrec 40651 dvconstbi 40659 zlmodzxzscm 44399 aacllem 44896 |
Copyright terms: Public domain | W3C validator |