Theorem fconst6g 6752

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

Syntax hints:   → wi 4   ∈ wcel 2109  {csn 4592   × cxp 5639  ⟶wf 6510

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-fun 6516  df-fn 6517  df-f 6518

This theorem is referenced by:  fconst6  6753  map0g  8860  fdiagfn  8866  mapsncnv  8869  brwdom2  9533  cantnf0  9635  fseqdom  9986  pwsdiagel  17467  setcmon  18056  setcepi  18057  pwsmnd  18706  pws0g  18707  0mhm  18753  pwspjmhm  18764  pwsgrp  18991  pwsinvg  18992  symgpssefmnd  19333  pwscmn  19800  pwsabl  19801  pwsring  20240  pws1  20241  pwscrng  20242  pwslmod  20883  frlmlmod  21665  frlmlss  21667  psrvscacl  21867  psr0cl  21868  psrlmod  21876  mplsubglem  21915  coe1fval3  22100  coe1z  22156  coe1mul2  22162  coe1tm  22166  evls1sca  22217  rhmply1vsca  22282  mamuvs1  22299  mamuvs2  22300  lmconst  23155  cnconst2  23177  pwstps  23524  xkopt  23549  xkopjcn  23550  tmdgsum  23989  tmdgsum2  23990  symgtgp  24000  cstucnd  24178  imasdsf1olem  24268  pwsxms  24427  pwsms  24428  mbfconstlem  25535  mbfmulc2lem  25555  i1fmulc  25611  itg2mulc  25655  dvconst  25825  dvcmul  25854  plypf1  26124  amgmlem  26907  dchrelbas2  27155  resf1o  32660  elrspunidl  33406  ofcccat  34541  lpadlem1  34675  poimirlem28  37649  lflvscl  39077  lflvsdi1  39078  lflvsdi2  39079  lflvsass  39081  evlsvvval  42558  fsuppssind  42588  mhphf  42592  constmap  42708  mendlmod  43185  cantnfresb  43320  ofoafo  43352  naddcnffo  43360  naddcnfid1  43363  naddcnfid2  43364  onnog  43425  dvsconst  44326  expgrowth  44331  mapssbi  45214  dvsinax  45918  amgmlemALT  49796