![]() |
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 6130 | . 2 ⊢ (𝐵 ∈ 𝑉 → (𝐴 × {𝐵}):𝐴⟶{𝐵}) | |
2 | ffn 6083 | . 2 ⊢ ((𝐴 × {𝐵}):𝐴⟶{𝐵} → (𝐴 × {𝐵}) Fn 𝐴) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝐵 ∈ 𝑉 → (𝐴 × {𝐵}) Fn 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2030 {csn 4210 × cxp 5141 Fn wfn 5921 ⟶wf 5922 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 ax-sep 4814 ax-nul 4822 ax-pr 4936 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1056 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-eu 2502 df-mo 2503 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-ne 2824 df-ral 2946 df-rab 2950 df-v 3233 df-dif 3610 df-un 3612 df-in 3614 df-ss 3621 df-nul 3949 df-if 4120 df-sn 4211 df-pr 4213 df-op 4217 df-br 4686 df-opab 4746 df-mpt 4763 df-id 5053 df-xp 5149 df-rel 5150 df-cnv 5151 df-co 5152 df-dm 5153 df-rn 5154 df-fun 5928 df-fn 5929 df-f 5930 |
This theorem is referenced by: fconst2g 6509 ofc1 6962 ofc2 6963 caofid0l 6967 caofid0r 6968 caofid1 6969 caofid2 6970 fnsuppres 7367 fczsupp0 7369 fczfsuppd 8334 brwdom2 8519 cantnf0 8610 ofnegsub 11056 ofsubge0 11057 pwsplusgval 16197 pwsmulrval 16198 pwsvscafval 16201 xpsc0 16267 xpsc1 16268 pwsco1mhm 17417 dprdsubg 18469 pwsmgp 18664 pwssplit1 19107 frlmpwsfi 20144 frlmbas 20147 frlmvscaval 20158 islindf4 20225 tmdgsum2 21947 0plef 23484 0pledm 23485 itg1ge0 23498 mbfi1fseqlem5 23531 xrge0f 23543 itg2ge0 23547 itg2addlem 23570 bddibl 23651 dvidlem 23724 rolle 23798 dveq0 23808 dv11cn 23809 tdeglem4 23865 mdeg0 23875 fta1blem 23973 qaa 24123 basellem9 24860 ofcc 30296 ofcof 30297 eulerpartlemt 30561 noextendseq 31945 matunitlindflem1 33535 matunitlindflem2 33536 ptrecube 33539 poimirlem1 33540 poimirlem2 33541 poimirlem3 33542 poimirlem4 33543 poimirlem5 33544 poimirlem6 33545 poimirlem7 33546 poimirlem10 33549 poimirlem11 33550 poimirlem12 33551 poimirlem16 33555 poimirlem17 33556 poimirlem19 33558 poimirlem20 33559 poimirlem22 33561 poimirlem23 33562 poimirlem28 33567 poimirlem29 33568 poimirlem31 33570 poimirlem32 33571 broucube 33573 cnpwstotbnd 33726 eqlkr2 34705 pwssplit4 37976 mpaaeu 38037 rngunsnply 38060 ofdivrec 38842 dvconstbi 38850 zlmodzxzscm 42460 aacllem 42875 |
Copyright terms: Public domain | W3C validator |