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

Theorem fnconstg 5778
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 5777 . 2
2 ffn 5736 . 2
31, 2syl 16 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  e.wcel 1818  {csn 4029  X.cxp 5002  Fnwfn 5588  -->wf 5589
This theorem is referenced by:  fconst2g  6125  fnsuppresOLD  6131  ofc1  6563  ofc2  6564  caofid0l  6568  caofid0r  6569  caofid1  6570  caofid2  6571  fnsuppres  6946  fczsupp0  6948  fczfsuppd  7867  brwdom2  8020  cantnf0  8115  ofnegsub  10559  ofsubge0  10560  pwsplusgval  14887  pwsmulrval  14888  pwsvscafval  14891  xpsc0  14957  xpsc1  14958  pwsco1mhm  16001  dprdsubg  17071  pwsmgp  17267  pwssplit1  17705  frlmpwsfi  18783  frlmbas  18786  frlmbasOLD  18787  frlmvscaval  18800  islindf4  18873  tmdgsum2  20595  0plef  22079  0pledm  22080  itg1ge0  22093  mbfi1fseqlem5  22126  xrge0f  22138  itg2ge0  22142  itg2addlem  22165  bddibl  22246  dvidlem  22319  rolle  22391  dveq0  22401  dv11cn  22402  tdeglem4  22458  mdeg0  22470  fta1blem  22569  qaa  22719  basellem9  23362  ofcc  28105  ofcof  28106  eulerpartlemt  28310  cnpwstotbnd  30293  pwssplit4  31035  mpaaeu  31099  rngunsnply  31122  ofdivrec  31231  dvconstbi  31239  zlmodzxzscm  32946  aacllem  33216  eqlkr2  34825
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pr 4691
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-br 4453  df-opab 4511  df-mpt 4512  df-id 4800  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-fun 5595  df-fn 5596  df-f 5597
  Copyright terms: Public domain W3C validator