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

Theorem fnconstg 5698
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 5697 . 2  |-  ( B  e.  V  ->  ( A  X.  { B }
) : A --> { B } )
2 ffn 5656 . 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 1836   {csn 3961    X. cxp 4928    Fn wfn 5508   -->wf 5509
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-9 1840  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2020  ax-ext 2374  ax-sep 4505  ax-nul 4513  ax-pr 4618
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-eu 2236  df-mo 2237  df-clab 2382  df-cleq 2388  df-clel 2391  df-nfc 2546  df-ne 2593  df-ral 2751  df-rex 2752  df-rab 2755  df-v 3053  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-nul 3729  df-if 3875  df-sn 3962  df-pr 3964  df-op 3968  df-br 4385  df-opab 4443  df-mpt 4444  df-id 4726  df-xp 4936  df-rel 4937  df-cnv 4938  df-co 4939  df-dm 4940  df-rn 4941  df-fun 5515  df-fn 5516  df-f 5517
This theorem is referenced by:  fconst2g  6046  fnsuppresOLD  6053  ofc1  6484  ofc2  6485  caofid0l  6489  caofid0r  6490  caofid1  6491  caofid2  6492  fnsuppres  6867  fczsupp0  6869  fczfsuppd  7784  brwdom2  7936  cantnf0  8029  ofnegsub  10472  ofsubge0  10473  pwsplusgval  14920  pwsmulrval  14921  pwsvscafval  14924  xpsc0  14990  xpsc1  14991  pwsco1mhm  16141  dprdsubg  17207  pwsmgp  17403  pwssplit1  17841  frlmpwsfi  18897  frlmbas  18900  frlmbasOLD  18901  frlmvscaval  18912  islindf4  18981  tmdgsum2  20703  0plef  22187  0pledm  22188  itg1ge0  22201  mbfi1fseqlem5  22234  xrge0f  22246  itg2ge0  22250  itg2addlem  22273  bddibl  22354  dvidlem  22427  rolle  22499  dveq0  22509  dv11cn  22510  tdeglem4  22566  mdeg0  22578  fta1blem  22677  qaa  22827  basellem9  23502  ofcc  28289  ofcof  28290  eulerpartlemt  28533  cnpwstotbnd  30499  pwssplit4  31241  mpaaeu  31307  rngunsnply  31330  ofdivrec  31439  dvconstbi  31447  zlmodzxzscm  33185  aacllem  33589  eqlkr2  35277
  Copyright terms: Public domain W3C validator