Theorem fconst6g 6749

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

Syntax hints:   → wi 4   ∈ wcel 2141  {csn 4581   × cxp 5643  ⟶wf 6513

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5245  ax-pr 5389

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5540  df-xp 5651  df-rel 5652  df-cnv 5653  df-co 5654  df-dm 5655  df-rn 5656  df-fun 6519  df-fn 6520  df-f 6521

This theorem is referenced by:  fconst6  6750  map0g  8862  fdiagfn  8868  mapsncnv  8871  brwdom2  9518  cantnf0  9627  fseqdom  9979  pwsdiagel  17510  setcmon  18103  setcepi  18104  pwsmnd  18789  pws0g  18790  0mhm  18836  pwspjmhm  18847  pwsgrp  19077  pwsinvg  19078  symgpssefmnd  19419  pwscmn  19886  pwsabl  19887  pwsring  20351  pws1  20352  pwscrng  20353  pwslmod  21017  frlmlmod  21781  frlmlss  21783  psrvscacl  21983  psr0cl  21984  psrlmod  21991  mplsubglem  22030  evlsvvval  22126  coe1fval3  22250  coe1z  22306  coe1mul2  22312  coe1tm  22316  evls1sca  22366  rhmply1vsca  22428  mamuvs1  22445  mamuvs2  22446  lmconst  23301  cnconst2  23323  pwstps  23670  xkopt  23695  xkopjcn  23696  tmdgsum  24135  tmdgsum2  24136  symgtgp  24146  cstucnd  24323  imasdsf1olem  24413  pwsxms  24572  pwsms  24573  mbfconstlem  25669  mbfmulc2lem  25689  i1fmulc  25745  itg2mulc  25789  dvconst  25959  dvcmul  25986  plypf1  26252  amgmlem  27031  dchrelbas2  27278  resf1o  32882  elrspunidl  33575  ofcccat  34801  lpadlem1  34938  poimirlem28  38111  lflvscl  39665  lflvsdi1  39666  lflvsdi2  39667  lflvsass  39669  fsuppssind  43139  mhphf  43143  constmap  43258  mendlmod  43730  cantnfresb  43865  ofoafo  43897  naddcnffo  43905  naddcnfid1  43908  naddcnfid2  43909  onnoxpg  43969  dvsconst  44870  expgrowth  44875  mapssbi  45753  dvsinax  46451  amgmlemALT  50388