Theorem fconst6g 6731

Description: Constant function with loose range. (Contributed by Stefan O'Rear, 1-Feb-2015.)

Assertion

Ref	Expression
fconst6g	⊢ (𝐵 ∈ 𝐶 → (𝐴 × {𝐵}):𝐴⟶𝐶)

Proof of Theorem fconst6g

Step	Hyp	Ref	Expression
1		fconstg 6729	. 2 ⊢ (𝐵 ∈ 𝐶 → (𝐴 × {𝐵}):𝐴⟶{𝐵})
2		snssi 4766	. 2 ⊢ (𝐵 ∈ 𝐶 → {𝐵} ⊆ 𝐶)
3	1, 2	fssd 6687	1 ⊢ (𝐵 ∈ 𝐶 → (𝐴 × {𝐵}):𝐴⟶𝐶)

Syntax hints:   → wi 4   ∈ wcel 2114  {csn 4582   × cxp 5630  ⟶wf 6496

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-fun 6502  df-fn 6503  df-f 6504

This theorem is referenced by:  fconst6  6732  map0g  8834  fdiagfn  8840  mapsncnv  8843  brwdom2  9490  cantnf0  9596  fseqdom  9948  pwsdiagel  17430  setcmon  18023  setcepi  18024  pwsmnd  18709  pws0g  18710  0mhm  18756  pwspjmhm  18767  pwsgrp  18994  pwsinvg  18995  symgpssefmnd  19337  pwscmn  19804  pwsabl  19805  pwsring  20271  pws1  20272  pwscrng  20273  pwslmod  20933  frlmlmod  21716  frlmlss  21718  psrvscacl  21919  psr0cl  21920  psrlmod  21927  mplsubglem  21966  evlsvvval  22060  coe1fval3  22161  coe1z  22217  coe1mul2  22223  coe1tm  22227  evls1sca  22279  rhmply1vsca  22344  mamuvs1  22361  mamuvs2  22362  lmconst  23217  cnconst2  23239  pwstps  23586  xkopt  23611  xkopjcn  23612  tmdgsum  24051  tmdgsum2  24052  symgtgp  24062  cstucnd  24239  imasdsf1olem  24329  pwsxms  24488  pwsms  24489  mbfconstlem  25596  mbfmulc2lem  25616  i1fmulc  25672  itg2mulc  25716  dvconst  25886  dvcmul  25915  plypf1  26185  amgmlem  26968  dchrelbas2  27216  resf1o  32819  elrspunidl  33520  ofcccat  34720  lpadlem1  34854  poimirlem28  37896  lflvscl  39450  lflvsdi1  39451  lflvsdi2  39452  lflvsass  39454  fsuppssind  42948  mhphf  42952  constmap  43067  mendlmod  43543  cantnfresb  43678  ofoafo  43710  naddcnffo  43718  naddcnfid1  43721  naddcnfid2  43722  onnoxpg  43782  dvsconst  44683  expgrowth  44688  mapssbi  45568  dvsinax  46268  amgmlemALT  50159