Theorem fconst6g 6723

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

Syntax hints:   → wi 4   ∈ wcel 2113  {csn 4580   × cxp 5622  ⟶wf 6488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-fun 6494  df-fn 6495  df-f 6496

This theorem is referenced by:  fconst6  6724  map0g  8822  fdiagfn  8828  mapsncnv  8831  brwdom2  9478  cantnf0  9584  fseqdom  9936  pwsdiagel  17418  setcmon  18011  setcepi  18012  pwsmnd  18697  pws0g  18698  0mhm  18744  pwspjmhm  18755  pwsgrp  18982  pwsinvg  18983  symgpssefmnd  19325  pwscmn  19792  pwsabl  19793  pwsring  20259  pws1  20260  pwscrng  20261  pwslmod  20921  frlmlmod  21704  frlmlss  21706  psrvscacl  21907  psr0cl  21908  psrlmod  21915  mplsubglem  21954  evlsvvval  22048  coe1fval3  22149  coe1z  22205  coe1mul2  22211  coe1tm  22215  evls1sca  22267  rhmply1vsca  22332  mamuvs1  22349  mamuvs2  22350  lmconst  23205  cnconst2  23227  pwstps  23574  xkopt  23599  xkopjcn  23600  tmdgsum  24039  tmdgsum2  24040  symgtgp  24050  cstucnd  24227  imasdsf1olem  24317  pwsxms  24476  pwsms  24477  mbfconstlem  25584  mbfmulc2lem  25604  i1fmulc  25660  itg2mulc  25704  dvconst  25874  dvcmul  25903  plypf1  26173  amgmlem  26956  dchrelbas2  27204  resf1o  32809  elrspunidl  33509  ofcccat  34700  lpadlem1  34834  poimirlem28  37849  lflvscl  39337  lflvsdi1  39338  lflvsdi2  39339  lflvsass  39341  fsuppssind  42836  mhphf  42840  constmap  42955  mendlmod  43431  cantnfresb  43566  ofoafo  43598  naddcnffo  43606  naddcnfid1  43609  naddcnfid2  43610  onnoxpg  43670  dvsconst  44571  expgrowth  44576  mapssbi  45457  dvsinax  46157  amgmlemALT  50048