Theorem fconst6g 6757

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

Syntax hints:   → wi 4   ∈ wcel 2145  {csn 4585   × cxp 5649  ⟶wf 6521

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5250  ax-pr 5394

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-br 5105  df-opab 5167  df-mpt 5186  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-fun 6527  df-fn 6528  df-f 6529

This theorem is referenced by:  fconst6  6758  map0g  8870  fdiagfn  8876  mapsncnv  8879  brwdom2  9523  cantnf0  9632  fseqdom  9998  pwsdiagel  17539  setcmon  18132  setcepi  18133  pwsmnd  18818  pws0g  18819  0mhm  18866  pwspjmhm  18877  pwsgrp  19106  pwsinvg  19107  symgpssefmnd  19454  pwscmn  19921  pwsabl  19922  pwsring  20393  pws1  20394  pwscrng  20395  pwslmod  21057  frlmlmod  21856  frlmlss  21858  psrvscacl  22058  psr0cl  22059  psrlmod  22066  mplsubglem  22105  evlsvvval  22201  coe1fval3  22325  coe1z  22381  coe1mul2  22387  coe1tm  22391  evls1sca  22440  rhmply1vsca  22502  mamuvs1  22519  mamuvs2  22520  lmconst  23375  cnconst2  23397  pwstps  23744  xkopt  23769  xkopjcn  23770  tmdgsum  24209  tmdgsum2  24210  symgtgp  24220  cstucnd  24397  imasdsf1olem  24487  pwsxms  24646  pwsms  24647  mbfconstlem  25743  mbfmulc2lem  25763  i1fmulc  25819  itg2mulc  25863  dvconst  26033  dvcmul  26060  plypf1  26326  amgmlem  27108  dchrelbas2  27355  resf1o  32983  elrspunidl  33647  ofcccat  34845  lpadlem1  34979  poimirlem28  38154  lflvscl  39708  lflvsdi1  39709  lflvsdi2  39710  lflvsass  39712  fsuppssind  43182  mhphf  43186  constmap  43301  mendlmod  43773  cantnfresb  43908  ofoafo  43940  naddcnffo  43948  naddcnfid1  43951  naddcnfid2  43952  onnoxpg  44012  dvsconst  44899  expgrowth  44904  mapssbi  45788  dvsinax  46486  amgmlemALT  50433