Theorem fconst6g 6719

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

Syntax hints:   → wi 4   ∈ wcel 2113  {csn 4577   × cxp 5619  ⟶wf 6484

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 2182  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pr 5374

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 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5516  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-fun 6490  df-fn 6491  df-f 6492

This theorem is referenced by:  fconst6  6720  map0g  8816  fdiagfn  8822  mapsncnv  8825  brwdom2  9468  cantnf0  9574  fseqdom  9926  pwsdiagel  17405  setcmon  17998  setcepi  17999  pwsmnd  18684  pws0g  18685  0mhm  18731  pwspjmhm  18742  pwsgrp  18969  pwsinvg  18970  symgpssefmnd  19312  pwscmn  19779  pwsabl  19780  pwsring  20246  pws1  20247  pwscrng  20248  pwslmod  20907  frlmlmod  21690  frlmlss  21692  psrvscacl  21892  psr0cl  21893  psrlmod  21900  mplsubglem  21939  coe1fval3  22124  coe1z  22180  coe1mul2  22186  coe1tm  22190  evls1sca  22241  rhmply1vsca  22306  mamuvs1  22323  mamuvs2  22324  lmconst  23179  cnconst2  23201  pwstps  23548  xkopt  23573  xkopjcn  23574  tmdgsum  24013  tmdgsum2  24014  symgtgp  24024  cstucnd  24201  imasdsf1olem  24291  pwsxms  24450  pwsms  24451  mbfconstlem  25558  mbfmulc2lem  25578  i1fmulc  25634  itg2mulc  25678  dvconst  25848  dvcmul  25877  plypf1  26147  amgmlem  26930  dchrelbas2  27178  resf1o  32719  elrspunidl  33402  ofcccat  34579  lpadlem1  34713  poimirlem28  37711  lflvscl  39199  lflvsdi1  39200  lflvsdi2  39201  lflvsass  39203  evlsvvval  42684  fsuppssind  42714  mhphf  42718  constmap  42833  mendlmod  43309  cantnfresb  43444  ofoafo  43476  naddcnffo  43484  naddcnfid1  43487  naddcnfid2  43488  onnog  43549  dvsconst  44450  expgrowth  44455  mapssbi  45337  dvsinax  46038  amgmlemALT  49931