Theorem fconst6g 6769

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

Syntax hints:   → wi 4   ∈ wcel 2143  {csn 4590   × cxp 5661  ⟶wf 6534

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-pr 5406

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-fun 6540  df-fn 6541  df-f 6542

This theorem is referenced by:  fconst6  6770  map0g  8883  fdiagfn  8889  mapsncnv  8892  brwdom2  9536  cantnf0  9645  fseqdom  10011  pwsdiagel  17552  setcmon  18145  setcepi  18146  pwsmnd  18831  pws0g  18832  0mhm  18879  pwspjmhm  18890  pwsgrp  19119  pwsinvg  19120  symgpssefmnd  19467  pwscmn  19934  pwsabl  19935  pwsring  20406  pws1  20407  pwscrng  20408  pwslmod  21072  frlmlmod  21880  frlmlss  21882  psrvscacl  22082  psr0cl  22083  psrlmod  22090  mplsubglem  22129  evlsvvval  22225  coe1fval3  22349  coe1z  22405  coe1mul2  22411  coe1tm  22415  evls1sca  22464  rhmply1vsca  22526  mamuvs1  22543  mamuvs2  22544  lmconst  23399  cnconst2  23421  pwstps  23768  xkopt  23793  xkopjcn  23794  tmdgsum  24233  tmdgsum2  24234  symgtgp  24244  cstucnd  24421  imasdsf1olem  24511  pwsxms  24670  pwsms  24671  mbfconstlem  25767  mbfmulc2lem  25787  i1fmulc  25843  itg2mulc  25887  dvconst  26057  dvcmul  26084  plypf1  26350  amgmlem  27135  dchrelbas2  27382  resf1o  33056  elrspunidl  33717  ofcccat  34914  lpadlem1  35048  poimirlem28  38280  lflvscl  39832  lflvsdi1  39833  lflvsdi2  39834  lflvsass  39836  fsuppssind  43308  mhphf  43312  constmap  43427  mendlmod  43899  cantnfresb  44034  ofoafo  44066  naddcnffo  44074  naddcnfid1  44077  naddcnfid2  44078  onnoxpg  44138  dvsconst  45023  expgrowth  45028  mapssbi  45912  dvsinax  46610  amgmlemALT  50586