MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fconst6g Structured version   Unicode version

Theorem fconst6g 5624
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
StepHypRef Expression
1 fconstg 5622 . 2  |-  ( B  e.  C  ->  ( A  X.  { B }
) : A --> { B } )
2 snssi 3934 . 2  |-  ( B  e.  C  ->  { B }  C_  C )
3 fss 5591 . 2  |-  ( ( ( A  X.  { B } ) : A --> { B }  /\  { B }  C_  C )  ->  ( A  X.  { B } ) : A --> C )
41, 2, 3syl2anc 643 1  |-  ( B  e.  C  ->  ( A  X.  { B }
) : A --> C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1725    C_ wss 3312   {csn 3806    X. cxp 4868   -->wf 5442
This theorem is referenced by:  fconst6  5625  map0g  7045  fdiagfn  7049  mapsncnv  7052  brwdom2  7533  cantnf0  7622  fseqdom  7899  pwsdiagel  13711  setcmon  14234  setcepi  14235  pwsmnd  14722  pws0g  14723  0mhm  14750  pwspjmhm  14759  pwsgrp  14921  pwsinvg  14922  pwscmn  15470  pwsabl  15471  dprdsubg  15574  pwsrng  15713  pws1  15714  pwscrng  15715  pwslmod  16038  psrvscacl  16449  psr0cl  16450  psrlmod  16457  mplsubglem  16490  coe1fval3  16598  coe1z  16648  coe1mul2  16654  coe1tm  16657  lmconst  17317  cnconst2  17339  pwstps  17654  xkopt  17679  xkopjcn  17680  tmdgsum  18117  tmdgsum2  18118  symgtgp  18123  cstucnd  18306  imasdsf1olem  18395  pwsxms  18554  pwsms  18555  mbfconstlem  19513  mbfmulc2lem  19531  i1fmulc  19587  itg2mulc  19631  dvconst  19795  dvcmul  19822  plypf1  20123  amgmlem  20820  dchrelbas2  21013  constmap  26758  frlmlmod  27185  frlmlss  27187  mamuvs1  27431  mamuvs2  27432  mendlmod  27469  dvsconst  27515  expgrowth  27520  lflvscl  29812  lflvsdi1  29813  lflvsdi2  29814  lflvsass  29816
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-sep 4322  ax-nul 4330  ax-pr 4395
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-ral 2702  df-rex 2703  df-rab 2706  df-v 2950  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-sn 3812  df-pr 3813  df-op 3815  df-br 4205  df-opab 4259  df-mpt 4260  df-id 4490  df-xp 4876  df-rel 4877  df-cnv 4878  df-co 4879  df-dm 4880  df-rn 4881  df-fun 5448  df-fn 5449  df-f 5450
  Copyright terms: Public domain W3C validator