Theorem fconst6g 5770

Description: Constant function with loose range. (Contributed by Stefan O'Rear, 1-Feb-2015.)

Assertion

Ref	Expression
fconst6g	|- ( B e. C -> ( A X. { B } ) : A --> C )

Proof of Theorem fconst6g

Step	Hyp	Ref	Expression
1		fconstg 5768	. 2 |- ( B e. C -> ( A X. { B } ) : A --> { B } )
2		snssi 4115	. 2 |- ( B e. C -> { B } C_ C )
3	1, 2	fssd 5736	1 |- ( B e. C -> ( A X. { B } ) : A --> C )

Syntax hints:   -> wi 4   e. wcel 1886   {csn 3967   X. cxp 4831   -->wf 5577

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-9 1895  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-sep 4524  ax-nul 4533  ax-pr 4638

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 986  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-eu 2302  df-mo 2303  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-ral 2741  df-rex 2742  df-rab 2745  df-v 3046  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-nul 3731  df-if 3881  df-sn 3968  df-pr 3970  df-op 3974  df-br 4402  df-opab 4461  df-mpt 4462  df-id 4748  df-xp 4839  df-rel 4840  df-cnv 4841  df-co 4842  df-dm 4843  df-rn 4844  df-fun 5583  df-fn 5584  df-f 5585

This theorem is referenced by:  fconst6  5771  map0g  7508  fdiagfn  7512  mapsncnv  7515  brwdom2  8085  cantnf0  8177  fseqdom  8454  pwsdiagel  15388  setcmon  15975  setcepi  15976  pwsmnd  16564  pws0g  16565  0mhm  16598  pwspjmhm  16608  pwsgrp  16790  pwsinvg  16791  pwscmn  17494  pwsabl  17495  pwsring  17836  pws1  17837  pwscrng  17838  pwslmod  18186  psrvscacl  18610  psr0cl  18611  psrlmod  18618  mplsubglem  18651  coe1fval3  18794  coe1z  18849  coe1mul2  18855  coe1tm  18859  evls1sca  18905  frlmlmod  19305  frlmlss  19307  mamuvs1  19423  mamuvs2  19424  lmconst  20270  cnconst2  20292  pwstps  20638  xkopt  20663  xkopjcn  20664  tmdgsum  21103  tmdgsum2  21104  symgtgp  21109  cstucnd  21292  imasdsf1olem  21381  pwsxms  21540  pwsms  21541  mbfconstlem  22578  mbfmulc2lem  22596  i1fmulc  22654  itg2mulc  22698  dvconst  22864  dvcmul  22891  plypf1  23159  amgmlem  23908  dchrelbas2  24158  resf1o  28308  ofcccat  29423  poimirlem28  31961  lflvscl  32637  lflvsdi1  32638  lflvsdi2  32639  lflvsass  32641  constmap  35549  mendlmod  36053  dvsconst  36673  expgrowth  36678  dvsinax  37777