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

Syntax hints:   → wi 4   ∈ wcel 2119  {csn 4562   × cxp 5623  ⟶wf 6488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-pr 5369

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-br 5080  df-opab 5142  df-mpt 5161  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-fun 6494  df-fn 6495  df-f 6496

This theorem is referenced by:  fconst6  6724  map0g  8829  fdiagfn  8835  mapsncnv  8838  brwdom2  9485  cantnf0  9594  fseqdom  9946  pwsdiagel  17459  setcmon  18052  setcepi  18053  pwsmnd  18738  pws0g  18739  0mhm  18785  pwspjmhm  18796  pwsgrp  19026  pwsinvg  19027  symgpssefmnd  19369  pwscmn  19836  pwsabl  19837  pwsring  20301  pws1  20302  pwscrng  20303  pwslmod  20967  frlmlmod  21731  frlmlss  21733  psrvscacl  21933  psr0cl  21934  psrlmod  21941  mplsubglem  21980  evlsvvval  22076  coe1fval3  22200  coe1z  22256  coe1mul2  22262  coe1tm  22266  evls1sca  22316  rhmply1vsca  22378  mamuvs1  22395  mamuvs2  22396  lmconst  23251  cnconst2  23273  pwstps  23620  xkopt  23645  xkopjcn  23646  tmdgsum  24085  tmdgsum2  24086  symgtgp  24096  cstucnd  24273  imasdsf1olem  24363  pwsxms  24522  pwsms  24523  mbfconstlem  25619  mbfmulc2lem  25639  i1fmulc  25695  itg2mulc  25739  dvconst  25909  dvcmul  25936  plypf1  26202  amgmlem  26978  dchrelbas2  27225  resf1o  32829  elrspunidl  33518  ofcccat  34734  lpadlem1  34868  poimirlem28  38022  lflvscl  39576  lflvsdi1  39577  lflvsdi2  39578  lflvsass  39580  fsuppssind  43050  mhphf  43054  constmap  43169  mendlmod  43641  cantnfresb  43776  ofoafo  43808  naddcnffo  43816  naddcnfid1  43819  naddcnfid2  43820  onnoxpg  43880  dvsconst  44781  expgrowth  44786  mapssbi  45665  dvsinax  46363  amgmlemALT  50300