Theorem fconst6g 6672

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

Syntax hints:   → wi 4   ∈ wcel 2107  {csn 4562   × cxp 5588  ⟶wf 6433

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-sep 5224  ax-nul 5231  ax-pr 5353

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-br 5076  df-opab 5138  df-mpt 5159  df-id 5490  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-fun 6439  df-fn 6440  df-f 6441

This theorem is referenced by:  fconst6  6673  map0g  8681  fdiagfn  8687  mapsncnv  8690  brwdom2  9341  cantnf0  9442  fseqdom  9791  pwsdiagel  17217  setcmon  17811  setcepi  17812  pwsmnd  18429  pws0g  18430  0mhm  18467  pwspjmhm  18477  pwsgrp  18696  pwsinvg  18697  symgpssefmnd  19012  pwscmn  19473  pwsabl  19474  pwsring  19863  pws1  19864  pwscrng  19865  pwslmod  20241  frlmlmod  20965  frlmlss  20967  psrvscacl  21171  psr0cl  21172  psrlmod  21179  mplsubglem  21214  coe1fval3  21388  coe1z  21443  coe1mul2  21449  coe1tm  21453  evls1sca  21498  mamuvs1  21561  mamuvs2  21562  lmconst  22421  cnconst2  22443  pwstps  22790  xkopt  22815  xkopjcn  22816  tmdgsum  23255  tmdgsum2  23256  symgtgp  23266  cstucnd  23445  imasdsf1olem  23535  pwsxms  23697  pwsms  23698  mbfconstlem  24800  mbfmulc2lem  24820  i1fmulc  24877  itg2mulc  24921  dvconst  25090  dvcmul  25117  plypf1  25382  amgmlem  26148  dchrelbas2  26394  resf1o  31074  elrspunidl  31615  ofcccat  32531  lpadlem1  32666  poimirlem28  35814  lflvscl  37098  lflvsdi1  37099  lflvsdi2  37100  lflvsass  37102  evlsbagval  40282  fsuppssind  40289  mhphf  40292  constmap  40542  mendlmod  41025  dvsconst  41955  expgrowth  41960  mapssbi  42760  dvsinax  43461  amgmlemALT  46518