Theorem fconst6g 6767

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

Syntax hints:   → wi 4   ∈ wcel 2108  {csn 4601   × cxp 5652  ⟶wf 6527

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 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-fun 6533  df-fn 6534  df-f 6535

This theorem is referenced by:  fconst6  6768  map0g  8898  fdiagfn  8904  mapsncnv  8907  brwdom2  9587  cantnf0  9689  fseqdom  10040  pwsdiagel  17511  setcmon  18100  setcepi  18101  pwsmnd  18750  pws0g  18751  0mhm  18797  pwspjmhm  18808  pwsgrp  19035  pwsinvg  19036  symgpssefmnd  19377  pwscmn  19844  pwsabl  19845  pwsring  20284  pws1  20285  pwscrng  20286  pwslmod  20927  frlmlmod  21709  frlmlss  21711  psrvscacl  21911  psr0cl  21912  psrlmod  21920  mplsubglem  21959  coe1fval3  22144  coe1z  22200  coe1mul2  22206  coe1tm  22210  evls1sca  22261  rhmply1vsca  22326  mamuvs1  22343  mamuvs2  22344  lmconst  23199  cnconst2  23221  pwstps  23568  xkopt  23593  xkopjcn  23594  tmdgsum  24033  tmdgsum2  24034  symgtgp  24044  cstucnd  24222  imasdsf1olem  24312  pwsxms  24471  pwsms  24472  mbfconstlem  25580  mbfmulc2lem  25600  i1fmulc  25656  itg2mulc  25700  dvconst  25870  dvcmul  25899  plypf1  26169  amgmlem  26952  dchrelbas2  27200  resf1o  32707  elrspunidl  33443  ofcccat  34575  lpadlem1  34709  poimirlem28  37672  lflvscl  39095  lflvsdi1  39096  lflvsdi2  39097  lflvsass  39099  evlsvvval  42586  fsuppssind  42616  mhphf  42620  constmap  42736  mendlmod  43213  cantnfresb  43348  ofoafo  43380  naddcnffo  43388  naddcnfid1  43391  naddcnfid2  43392  onnog  43453  dvsconst  44354  expgrowth  44359  mapssbi  45237  dvsinax  45942  amgmlemALT  49667