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

Theorem fnconstg 5764
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 5763 . 2  |-  ( B  e.  V  ->  ( A  X.  { B }
) : A --> { B } )
2 ffn 5722 . 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 1762   {csn 4020    X. cxp 4990    Fn wfn 5574   -->wf 5575
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-sep 4561  ax-nul 4569  ax-pr 4679
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-eu 2272  df-mo 2273  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3108  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-sn 4021  df-pr 4023  df-op 4027  df-br 4441  df-opab 4499  df-mpt 4500  df-id 4788  df-xp 4998  df-rel 4999  df-cnv 5000  df-co 5001  df-dm 5002  df-rn 5003  df-fun 5581  df-fn 5582  df-f 5583
This theorem is referenced by:  fconst2g  6106  fnsuppresOLD  6112  ofc1  6538  ofc2  6539  caofid0l  6543  caofid0r  6544  caofid1  6545  caofid2  6546  fnsuppres  6917  fczsupp0  6919  fczfsuppd  7836  brwdom2  7988  cantnf0  8083  ofnegsub  10523  ofsubge0  10524  pwsplusgval  14734  pwsmulrval  14735  pwsvscafval  14738  xpsc0  14804  xpsc1  14805  pwsco1mhm  15804  dprdsubg  16854  pwsmgp  17044  pwssplit1  17481  frlmpwsfi  18543  frlmbas  18546  frlmbasOLD  18547  frlmvscaval  18560  islindf4  18633  tmdgsum2  20323  0plef  21807  0pledm  21808  itg1ge0  21821  mbfi1fseqlem5  21854  xrge0f  21866  itg2ge0  21870  itg2addlem  21893  bddibl  21974  dvidlem  22047  rolle  22119  dveq0  22129  dv11cn  22130  tdeglem4  22186  mdeg0  22198  fta1blem  22297  qaa  22446  basellem9  23083  ofcc  27731  ofcof  27732  eulerpartlemt  27936  cnpwstotbnd  29883  pwssplit4  30628  mpaaeu  30693  rngunsnply  30716  ofdivrec  30786  dvconstbi  30794  zlmodzxzscm  31885  eqlkr2  33772
  Copyright terms: Public domain W3C validator