![]() |
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 6774 | . 2 ⊢ (𝐵 ∈ 𝑉 → (𝐴 × {𝐵}):𝐴⟶{𝐵}) | |
2 | 1 | ffnd 6714 | 1 ⊢ (𝐵 ∈ 𝑉 → (𝐴 × {𝐵}) Fn 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2107 {csn 4626 × cxp 5672 Fn wfn 6534 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-sep 5297 ax-nul 5304 ax-pr 5425 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-ral 3063 df-rex 3072 df-rab 3434 df-v 3477 df-dif 3949 df-un 3951 df-in 3953 df-ss 3963 df-nul 4321 df-if 4527 df-sn 4627 df-pr 4629 df-op 4633 df-br 5147 df-opab 5209 df-mpt 5230 df-id 5572 df-xp 5680 df-rel 5681 df-cnv 5682 df-co 5683 df-dm 5684 df-rn 5685 df-fun 6541 df-fn 6542 df-f 6543 |
This theorem is referenced by: fconst2g 7198 ofc1 7690 ofc2 7691 caofid0l 7695 caofid0r 7696 caofid1 7697 caofid2 7698 fnsuppres 8170 fczsupp0 8172 fczfsuppd 9376 brwdom2 9563 cantnf0 9665 ofnegsub 12205 ofsubge0 12206 pwsplusgval 17431 pwsmulrval 17432 pwsvscafval 17435 pwsco1mhm 18708 dprdsubg 19885 pwsmgp 20129 pwssplit1 20657 frlmpwsfi 21290 frlmbas 21293 frlmvscaval 21306 islindf4 21376 tmdgsum2 23581 0plef 25170 0pledm 25171 itg1ge0 25184 mbfi1fseqlem5 25218 xrge0f 25230 itg2ge0 25234 itg2addlem 25257 bddibl 25338 dvidlem 25413 rolle 25488 dveq0 25498 dv11cn 25499 tdeglem4 25558 tdeglem4OLD 25559 mdeg0 25569 fta1blem 25667 qaa 25817 basellem9 26572 noextendseq 27149 noetainflem4 27222 fdifsuppconst 31888 elrspunidl 32503 ofcc 33041 ofcof 33042 eulerpartlemt 33307 matunitlindflem1 36421 matunitlindflem2 36422 ptrecube 36425 poimirlem1 36426 poimirlem2 36427 poimirlem3 36428 poimirlem4 36429 poimirlem5 36430 poimirlem6 36431 poimirlem7 36432 poimirlem10 36435 poimirlem11 36436 poimirlem12 36437 poimirlem16 36441 poimirlem17 36442 poimirlem19 36444 poimirlem20 36445 poimirlem22 36447 poimirlem23 36448 poimirlem28 36453 poimirlem29 36454 poimirlem31 36456 poimirlem32 36457 broucube 36459 cnpwstotbnd 36602 eqlkr2 37907 fsuppssind 41114 pwssplit4 41763 mpaaeu 41824 rngunsnply 41847 ofoaid1 42040 ofoaid2 42041 naddcnffo 42046 ofdivrec 43017 dvconstbi 43025 zlmodzxzscm 46934 aacllem 47749 |
Copyright terms: Public domain | W3C validator |