Theorem fnconstg 6796

Description: A Cartesian product with a singleton is a constant function. (Contributed by NM, 24-Jul-2014.)

Assertion

Ref	Expression
fnconstg	⊢ (𝐵 ∈ 𝑉 → (𝐴 × {𝐵}) Fn 𝐴)

Proof of Theorem fnconstg

Step	Hyp	Ref	Expression
1		fconstg 6795	. 2 ⊢ (𝐵 ∈ 𝑉 → (𝐴 × {𝐵}):𝐴⟶{𝐵})
2	1	ffnd 6737	1 ⊢ (𝐵 ∈ 𝑉 → (𝐴 × {𝐵}) Fn 𝐴)

Syntax hints:   → wi 4   ∈ wcel 2105  {csn 4630   × cxp 5686   Fn wfn 6557

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-fun 6564  df-fn 6565  df-f 6566

This theorem is referenced by:  fconst2g  7222  ofc1  7724  ofc2  7725  caofid0l  7729  caofid0r  7730  caofid1  7731  caofid2  7732  fnsuppres  8214  fczsupp0  8216  fczfsuppd  9423  brwdom2  9610  cantnf0  9712  ofnegsub  12261  ofsubge0  12262  pwsplusgval  17536  pwsmulrval  17537  pwsvscafval  17540  pwsco1mhm  18857  dprdsubg  20058  pwsmgp  20340  pwssplit1  21075  frlmpwsfi  21789  frlmbas  21792  frlmvscaval  21805  islindf4  21875  psrascl  22016  tmdgsum2  24119  0plef  25720  0pledm  25721  itg1ge0  25734  mbfi1fseqlem5  25768  xrge0f  25780  itg2ge0  25784  itg2addlem  25807  bddibl  25889  dvidlem  25964  rolle  26042  dveq0  26053  dv11cn  26054  tdeglem4  26113  mdeg0  26123  fta1blem  26224  qaa  26379  basellem9  27146  noextendseq  27726  noetainflem4  27799  fdifsuppconst  32703  elrspunidl  33435  ofcc  34086  ofcof  34087  eulerpartlemt  34352  matunitlindflem1  37602  matunitlindflem2  37603  ptrecube  37606  poimirlem1  37607  poimirlem2  37608  poimirlem3  37609  poimirlem4  37610  poimirlem5  37611  poimirlem6  37612  poimirlem7  37613  poimirlem10  37616  poimirlem11  37617  poimirlem12  37618  poimirlem16  37622  poimirlem17  37623  poimirlem19  37625  poimirlem20  37626  poimirlem22  37628  poimirlem23  37629  poimirlem28  37634  poimirlem29  37635  poimirlem31  37637  poimirlem32  37638  broucube  37640  cnpwstotbnd  37783  eqlkr2  39081  fsuppssind  42579  pwssplit4  43077  mpaaeu  43138  rngunsnply  43157  ofoaid1  43347  ofoaid2  43348  naddcnffo  43353  ofdivrec  44321  dvconstbi  44329  zlmodzxzscm  48201  aacllem  49031