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

Theorem fnconstg 5568
Description: A Cartesian product with a singleton is a constant function. (Contributed by NM, 24-Jul-2014.)
Assertion
Ref Expression
fnconstg

Proof of Theorem fnconstg
StepHypRef Expression
1 fconstg 5567 . 2
2 ffn 5529 . 2
31, 2syl 16 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  e.wcel 1749  {csn 3853  X.cxp 4809  Fnwfn 5385  -->wf 5386
This theorem is referenced by:  fconst2g  5901  fnsuppresOLD  5907  ofc1  6313  ofc2  6314  caofid0l  6318  caofid0r  6319  caofid1  6320  caofid2  6321  fnsuppres  6681  fczsupp0  6683  fczfsuppd  7594  brwdom2  7735  cantnf0  7830  ofnegsub  10266  ofsubge0  10267  pwsplusgval  14368  pwsmulrval  14369  pwsvscafval  14372  xpsc0  14438  xpsc1  14439  pwsco1mhm  15437  dprdsubg  16391  pwsmgp  16534  pwssplit1  16949  frlmpwsfi  17885  frlmbas  17888  frlmvscaval  17900  islindf4  17966  tmdgsum2  19371  0plef  20850  0pledm  20851  itg1ge0  20864  mbfi1fseqlem5  20897  xrge0f  20909  itg2ge0  20913  itg2addlem  20936  bddibl  21017  dvidlem  21090  rolle  21162  dveq0  21172  dv11cn  21173  tdeglem4  21271  fta1blem  21381  qaa  21530  basellem9  22167  ofcc  26257  ofcof  26258  eulerpartlemt  26457  cnpwstotbnd  28367  pwssplit4  29115  mpaaeu  29180  rngunsnply  29203  ofdivrec  29273  dvconstbi  29281  zlmodzxzscm  30416  frlmXbas  30513  eqlkr2  32182
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1586  ax-4 1597  ax-5 1661  ax-6 1701  ax-7 1721  ax-9 1753  ax-10 1768  ax-11 1773  ax-12 1785  ax-13 1934  ax-ext 2403  ax-sep 4388  ax-nul 4396  ax-pr 4503
This theorem depends on definitions:  df-bi 179  df-or 363  df-an 364  df-3an 952  df-tru 1355  df-ex 1582  df-nf 1585  df-sb 1694  df-eu 2248  df-mo 2249  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2547  df-ne 2587  df-ral 2699  df-rex 2700  df-rab 2703  df-v 2953  df-dif 3308  df-un 3310  df-in 3312  df-ss 3319  df-nul 3615  df-if 3769  df-sn 3859  df-pr 3860  df-op 3862  df-br 4268  df-opab 4326  df-mpt 4327  df-id 4607  df-xp 4817  df-rel 4818  df-cnv 4819  df-co 4820  df-dm 4821  df-rn 4822  df-fun 5392  df-fn 5393  df-f 5394
  Copyright terms: Public domain W3C validator