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

Theorem fnconstg 5598
Description: A Cartesian product with a singleton is a constant function. (Contributed by NM, 24-Jul-2014.)
Assertion
Ref Expression
fnconstg  |-  ( B  e.  V  ->  ( A  X.  { B }
)  Fn  A )

Proof of Theorem fnconstg
StepHypRef Expression
1 fconstg 5597 . 2  |-  ( B  e.  V  ->  ( A  X.  { B }
) : A --> { B } )
2 ffn 5559 . 2  |-  ( ( A  X.  { B } ) : A --> { B }  ->  ( A  X.  { B }
)  Fn  A )
31, 2syl 16 1  |-  ( B  e.  V  ->  ( A  X.  { B }
)  Fn  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1756   {csn 3877    X. cxp 4838    Fn wfn 5413   -->wf 5414
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4413  ax-nul 4421  ax-pr 4531
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-ral 2720  df-rex 2721  df-rab 2724  df-v 2974  df-dif 3331  df-un 3333  df-in 3335  df-ss 3342  df-nul 3638  df-if 3792  df-sn 3878  df-pr 3880  df-op 3884  df-br 4293  df-opab 4351  df-mpt 4352  df-id 4636  df-xp 4846  df-rel 4847  df-cnv 4848  df-co 4849  df-dm 4850  df-rn 4851  df-fun 5420  df-fn 5421  df-f 5422
This theorem is referenced by:  fconst2g  5932  fnsuppresOLD  5938  ofc1  6343  ofc2  6344  caofid0l  6348  caofid0r  6349  caofid1  6350  caofid2  6351  fnsuppres  6716  fczsupp0  6718  fczfsuppd  7638  brwdom2  7788  cantnf0  7883  ofnegsub  10320  ofsubge0  10321  pwsplusgval  14428  pwsmulrval  14429  pwsvscafval  14432  xpsc0  14498  xpsc1  14499  pwsco1mhm  15498  dprdsubg  16521  pwsmgp  16710  pwssplit1  17140  frlmpwsfi  18177  frlmbas  18180  frlmbasOLD  18181  frlmvscaval  18194  islindf4  18267  tmdgsum2  19667  0plef  21150  0pledm  21151  itg1ge0  21164  mbfi1fseqlem5  21197  xrge0f  21209  itg2ge0  21213  itg2addlem  21236  bddibl  21317  dvidlem  21390  rolle  21462  dveq0  21472  dv11cn  21473  tdeglem4  21529  mdeg0  21541  fta1blem  21640  qaa  21789  basellem9  22426  ofcc  26548  ofcof  26549  eulerpartlemt  26754  cnpwstotbnd  28696  pwssplit4  29442  mpaaeu  29507  rngunsnply  29530  ofdivrec  29600  dvconstbi  29608  zlmodzxzscm  30754  eqlkr2  32745
  Copyright terms: Public domain W3C validator