Theorem fconst6g 5587

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 5585	. 2 |- ( B e. C -> ( A X. { B } ) : A --> { B } )
2		snssi 4005	. 2 |- ( B e. C -> { B } C_ C )
3		fss 5555	. 2 |- ( ( ( A X. { B } ) : A --> { B } /\ { B } C_ C ) -> ( A X. { B } ) : A --> C )
4	1, 2, 3	syl2anc 654	1 |- ( B e. C -> ( A X. { B } ) : A --> C )

Syntax hints:   -> wi 4   e. wcel 1755   C_ wss 3316   {csn 3865   X. cxp 4825   -->wf 5402

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pr 4519

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2964  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-br 4281  df-opab 4339  df-mpt 4340  df-id 4623  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-rn 4838  df-fun 5408  df-fn 5409  df-f 5410

This theorem is referenced by:  fconst6  5588  map0g  7240  fdiagfn  7244  mapsncnv  7247  brwdom2  7776  cantnf0  7871  fseqdom  8184  pwsdiagel  14418  setcmon  14938  setcepi  14939  pwsmnd  15439  pws0g  15440  0mhm  15468  pwspjmhm  15478  pwsgrp  15646  pwsinvg  15647  pwscmn  16325  pwsabl  16326  pwsrng  16642  pws1  16643  pwscrng  16644  pwslmod  16973  psrvscacl  17398  psr0cl  17399  psrlmod  17406  mplsubglem  17444  mplsubglemOLD  17446  coe1fval3  17563  coe1z  17615  coe1mul2  17621  coe1tm  17624  frlmlmod  18016  frlmlss  18018  mamuvs1  18151  mamuvs2  18152  lmconst  18707  cnconst2  18729  pwstps  19045  xkopt  19070  xkopjcn  19071  tmdgsum  19508  tmdgsum2  19509  symgtgp  19514  cstucnd  19701  imasdsf1olem  19790  pwsxms  19949  pwsms  19950  mbfconstlem  20949  mbfmulc2lem  20967  i1fmulc  21023  itg2mulc  21067  dvconst  21233  dvcmul  21260  plypf1  21565  amgmlem  22268  dchrelbas2  22461  ofcccat  26790  constmap  28894  mendlmod  29395  dvsconst  29449  expgrowth  29454  lflvscl  32316  lflvsdi1  32317  lflvsdi2  32318  lflvsass  32320