Theorem fconst6g 6779

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

Syntax hints:   → wi 4   ∈ wcel 2104  {csn 4627   × cxp 5673  ⟶wf 6538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pr 5426

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-fun 6544  df-fn 6545  df-f 6546

This theorem is referenced by:  fconst6  6780  map0g  8880  fdiagfn  8886  mapsncnv  8889  brwdom2  9570  cantnf0  9672  fseqdom  10023  pwsdiagel  17447  setcmon  18041  setcepi  18042  pwsmnd  18694  pws0g  18695  0mhm  18736  pwspjmhm  18747  pwsgrp  18971  pwsinvg  18972  symgpssefmnd  19304  pwscmn  19772  pwsabl  19773  pwsring  20212  pws1  20213  pwscrng  20214  pwslmod  20725  frlmlmod  21523  frlmlss  21525  psrvscacl  21731  psr0cl  21732  psrlmod  21740  mplsubglem  21777  coe1fval3  21951  coe1z  22005  coe1mul2  22011  coe1tm  22015  evls1sca  22062  mamuvs1  22125  mamuvs2  22126  lmconst  22985  cnconst2  23007  pwstps  23354  xkopt  23379  xkopjcn  23380  tmdgsum  23819  tmdgsum2  23820  symgtgp  23830  cstucnd  24009  imasdsf1olem  24099  pwsxms  24261  pwsms  24262  mbfconstlem  25376  mbfmulc2lem  25396  i1fmulc  25453  itg2mulc  25497  dvconst  25666  dvcmul  25695  plypf1  25961  amgmlem  26730  dchrelbas2  26976  resf1o  32222  elrspunidl  32820  ofcccat  33852  lpadlem1  33987  poimirlem28  36819  lflvscl  38250  lflvsdi1  38251  lflvsdi2  38252  lflvsass  38254  evlsvvval  41437  fsuppssind  41467  mhphf  41471  constmap  41753  mendlmod  42237  cantnfresb  42376  ofoafo  42408  naddcnffo  42416  naddcnfid1  42419  naddcnfid2  42420  onnog  42482  dvsconst  43391  expgrowth  43396  mapssbi  44210  dvsinax  44927  amgmlemALT  47937