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

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

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 5231  ax-pr 5370

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 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-mpt 5168  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  8825  fdiagfn  8831  mapsncnv  8834  brwdom2  9481  cantnf0  9587  fseqdom  9939  pwsdiagel  17452  setcmon  18045  setcepi  18046  pwsmnd  18731  pws0g  18732  0mhm  18778  pwspjmhm  18789  pwsgrp  19019  pwsinvg  19020  symgpssefmnd  19362  pwscmn  19829  pwsabl  19830  pwsring  20294  pws1  20295  pwscrng  20296  pwslmod  20956  frlmlmod  21739  frlmlss  21741  psrvscacl  21940  psr0cl  21941  psrlmod  21948  mplsubglem  21987  evlsvvval  22081  coe1fval3  22182  coe1z  22238  coe1mul2  22244  coe1tm  22248  evls1sca  22298  rhmply1vsca  22363  mamuvs1  22380  mamuvs2  22381  lmconst  23236  cnconst2  23258  pwstps  23605  xkopt  23630  xkopjcn  23631  tmdgsum  24070  tmdgsum2  24071  symgtgp  24081  cstucnd  24258  imasdsf1olem  24348  pwsxms  24507  pwsms  24508  mbfconstlem  25604  mbfmulc2lem  25624  i1fmulc  25680  itg2mulc  25724  dvconst  25894  dvcmul  25921  plypf1  26187  amgmlem  26967  dchrelbas2  27214  resf1o  32818  elrspunidl  33503  ofcccat  34703  lpadlem1  34837  poimirlem28  37983  lflvscl  39537  lflvsdi1  39538  lflvsdi2  39539  lflvsass  39541  fsuppssind  43040  mhphf  43044  constmap  43159  mendlmod  43635  cantnfresb  43770  ofoafo  43802  naddcnffo  43810  naddcnfid1  43813  naddcnfid2  43814  onnoxpg  43874  dvsconst  44775  expgrowth  44780  mapssbi  45660  dvsinax  46359  amgmlemALT  50290