Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > fconst6g | Structured version Visualization version GIF version |
Description: Constant function with loose range. (Contributed by Stefan O'Rear, 1-Feb-2015.) |
Ref | Expression |
---|---|
fconst6g | ⊢ (𝐵 ∈ 𝐶 → (𝐴 × {𝐵}):𝐴⟶𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fconstg 6566 | . 2 ⊢ (𝐵 ∈ 𝐶 → (𝐴 × {𝐵}):𝐴⟶{𝐵}) | |
2 | snssi 4697 | . 2 ⊢ (𝐵 ∈ 𝐶 → {𝐵} ⊆ 𝐶) | |
3 | 1, 2 | fssd 6523 | 1 ⊢ (𝐵 ∈ 𝐶 → (𝐴 × {𝐵}):𝐴⟶𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2114 {csn 4517 × cxp 5524 ⟶wf 6336 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2162 ax-12 2179 ax-ext 2711 ax-sep 5168 ax-nul 5175 ax-pr 5297 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-nf 1791 df-sb 2075 df-mo 2541 df-eu 2571 df-clab 2718 df-cleq 2731 df-clel 2812 df-nfc 2882 df-ne 2936 df-ral 3059 df-v 3401 df-dif 3847 df-un 3849 df-in 3851 df-ss 3861 df-nul 4213 df-if 4416 df-sn 4518 df-pr 4520 df-op 4524 df-br 5032 df-opab 5094 df-mpt 5112 df-id 5430 df-xp 5532 df-rel 5533 df-cnv 5534 df-co 5535 df-dm 5536 df-rn 5537 df-fun 6342 df-fn 6343 df-f 6344 |
This theorem is referenced by: fconst6 6569 map0g 8497 fdiagfn 8503 mapsncnv 8506 brwdom2 9113 cantnf0 9214 fseqdom 9529 pwsdiagel 16876 setcmon 17462 setcepi 17463 pwsmnd 18065 pws0g 18066 0mhm 18103 pwspjmhm 18113 pwsgrp 18332 pwsinvg 18333 symgpssefmnd 18645 pwscmn 19105 pwsabl 19106 pwsring 19490 pws1 19491 pwscrng 19492 pwslmod 19864 frlmlmod 20568 frlmlss 20570 psrvscacl 20775 psr0cl 20776 psrlmod 20783 mplsubglem 20818 coe1fval3 20986 coe1z 21041 coe1mul2 21047 coe1tm 21051 evls1sca 21096 mamuvs1 21159 mamuvs2 21160 lmconst 22015 cnconst2 22037 pwstps 22384 xkopt 22409 xkopjcn 22410 tmdgsum 22849 tmdgsum2 22850 symgtgp 22860 cstucnd 23039 imasdsf1olem 23129 pwsxms 23288 pwsms 23289 mbfconstlem 24382 mbfmulc2lem 24402 i1fmulc 24459 itg2mulc 24503 dvconst 24672 dvcmul 24699 plypf1 24964 amgmlem 25730 dchrelbas2 25976 resf1o 30643 elrspunidl 31181 ofcccat 32095 lpadlem1 32230 poimirlem28 35451 lflvscl 36737 lflvsdi1 36738 lflvsdi2 36739 lflvsass 36741 evlsbagval 39877 fsuppssind 39884 mhphf 39887 constmap 40130 mendlmod 40613 dvsconst 41509 expgrowth 41514 mapssbi 42314 dvsinax 43019 amgmlemALT 45990 |
Copyright terms: Public domain | W3C validator |