Theorem fconst6g 5706

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 5704	. 2 |- ( B e. C -> ( A X. { B } ) : A --> { B } )
2		snssi 4124	. 2 |- ( B e. C -> { B } C_ C )
3		fss 5674	. 2 |- ( ( ( A X. { B } ) : A --> { B } /\ { B } C_ C ) -> ( A X. { B } ) : A --> C )
4	1, 2, 3	syl2anc 661	1 |- ( B e. C -> ( A X. { B } ) : A --> C )

Syntax hints:   -> wi 4   e. wcel 1758   C_ wss 3435   {csn 3984   X. cxp 4945   -->wf 5521

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4520  ax-nul 4528  ax-pr 4638

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2649  df-ral 2803  df-rex 2804  df-rab 2807  df-v 3078  df-dif 3438  df-un 3440  df-in 3442  df-ss 3449  df-nul 3745  df-if 3899  df-sn 3985  df-pr 3987  df-op 3991  df-br 4400  df-opab 4458  df-mpt 4459  df-id 4743  df-xp 4953  df-rel 4954  df-cnv 4955  df-co 4956  df-dm 4957  df-rn 4958  df-fun 5527  df-fn 5528  df-f 5529

This theorem is referenced by:  fconst6  5707  map0g  7361  fdiagfn  7365  mapsncnv  7368  brwdom2  7898  cantnf0  7993  fseqdom  8306  pwsdiagel  14553  setcmon  15073  setcepi  15074  pwsmnd  15574  pws0g  15575  0mhm  15604  pwspjmhm  15614  pwsgrp  15784  pwsinvg  15785  pwscmn  16465  pwsabl  16466  pwsrng  16829  pws1  16830  pwscrng  16831  pwslmod  17173  psrvscacl  17586  psr0cl  17587  psrlmod  17594  mplsubglem  17633  mplsubglemOLD  17635  coe1fval3  17787  coe1z  17839  coe1mul2  17845  coe1tm  17849  evls1sca  17882  frlmlmod  18298  frlmlss  18300  mamuvs1  18433  mamuvs2  18434  lmconst  18996  cnconst2  19018  pwstps  19334  xkopt  19359  xkopjcn  19360  tmdgsum  19797  tmdgsum2  19798  symgtgp  19803  cstucnd  19990  imasdsf1olem  20079  pwsxms  20238  pwsms  20239  mbfconstlem  21239  mbfmulc2lem  21257  i1fmulc  21313  itg2mulc  21357  dvconst  21523  dvcmul  21550  plypf1  21812  amgmlem  22515  dchrelbas2  22708  ofcccat  27085  constmap  29196  mendlmod  29697  dvsconst  29751  expgrowth  29756  lflvscl  33045  lflvsdi1  33046  lflvsdi2  33047  lflvsass  33049