Theorem fconst6g 6647

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 6645	. 2 ⊢ (𝐵 ∈ 𝐶 → (𝐴 × {𝐵}):𝐴⟶{𝐵})
2		snssi 4738	. 2 ⊢ (𝐵 ∈ 𝐶 → {𝐵} ⊆ 𝐶)
3	1, 2	fssd 6602	1 ⊢ (𝐵 ∈ 𝐶 → (𝐴 × {𝐵}):𝐴⟶𝐶)

Syntax hints:   → wi 4   ∈ wcel 2108  {csn 4558   × cxp 5578  ⟶wf 6414

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-fun 6420  df-fn 6421  df-f 6422

This theorem is referenced by:  fconst6  6648  map0g  8630  fdiagfn  8636  mapsncnv  8639  brwdom2  9262  cantnf0  9363  fseqdom  9713  pwsdiagel  17125  setcmon  17718  setcepi  17719  pwsmnd  18335  pws0g  18336  0mhm  18373  pwspjmhm  18383  pwsgrp  18602  pwsinvg  18603  symgpssefmnd  18918  pwscmn  19379  pwsabl  19380  pwsring  19769  pws1  19770  pwscrng  19771  pwslmod  20147  frlmlmod  20866  frlmlss  20868  psrvscacl  21072  psr0cl  21073  psrlmod  21080  mplsubglem  21115  coe1fval3  21289  coe1z  21344  coe1mul2  21350  coe1tm  21354  evls1sca  21399  mamuvs1  21462  mamuvs2  21463  lmconst  22320  cnconst2  22342  pwstps  22689  xkopt  22714  xkopjcn  22715  tmdgsum  23154  tmdgsum2  23155  symgtgp  23165  cstucnd  23344  imasdsf1olem  23434  pwsxms  23594  pwsms  23595  mbfconstlem  24696  mbfmulc2lem  24716  i1fmulc  24773  itg2mulc  24817  dvconst  24986  dvcmul  25013  plypf1  25278  amgmlem  26044  dchrelbas2  26290  resf1o  30967  elrspunidl  31508  ofcccat  32422  lpadlem1  32557  poimirlem28  35732  lflvscl  37018  lflvsdi1  37019  lflvsdi2  37020  lflvsass  37022  evlsbagval  40198  fsuppssind  40205  mhphf  40208  constmap  40451  mendlmod  40934  dvsconst  41837  expgrowth  41842  mapssbi  42642  dvsinax  43344  amgmlemALT  46393