Theorem fconst6g 6810

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

Syntax hints:   → wi 4   ∈ wcel 2108  {csn 4648   × cxp 5698  ⟶wf 6569

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-fun 6575  df-fn 6576  df-f 6577

This theorem is referenced by:  fconst6  6811  map0g  8942  fdiagfn  8948  mapsncnv  8951  brwdom2  9642  cantnf0  9744  fseqdom  10095  pwsdiagel  17557  setcmon  18154  setcepi  18155  pwsmnd  18807  pws0g  18808  0mhm  18854  pwspjmhm  18865  pwsgrp  19092  pwsinvg  19093  symgpssefmnd  19437  pwscmn  19905  pwsabl  19906  pwsring  20347  pws1  20348  pwscrng  20349  pwslmod  20991  frlmlmod  21792  frlmlss  21794  psrvscacl  21994  psr0cl  21995  psrlmod  22003  mplsubglem  22042  coe1fval3  22231  coe1z  22287  coe1mul2  22293  coe1tm  22297  evls1sca  22348  rhmply1vsca  22413  mamuvs1  22430  mamuvs2  22431  lmconst  23290  cnconst2  23312  pwstps  23659  xkopt  23684  xkopjcn  23685  tmdgsum  24124  tmdgsum2  24125  symgtgp  24135  cstucnd  24314  imasdsf1olem  24404  pwsxms  24566  pwsms  24567  mbfconstlem  25681  mbfmulc2lem  25701  i1fmulc  25758  itg2mulc  25802  dvconst  25972  dvcmul  26001  plypf1  26271  amgmlem  27051  dchrelbas2  27299  resf1o  32744  elrspunidl  33421  ofcccat  34520  lpadlem1  34654  poimirlem28  37608  lflvscl  39033  lflvsdi1  39034  lflvsdi2  39035  lflvsass  39037  evlsvvval  42518  fsuppssind  42548  mhphf  42552  constmap  42669  mendlmod  43150  cantnfresb  43286  ofoafo  43318  naddcnffo  43326  naddcnfid1  43329  naddcnfid2  43330  onnog  43391  dvsconst  44299  expgrowth  44304  mapssbi  45120  dvsinax  45834  amgmlemALT  48897