Theorem fnconstg 6775

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 6774	. 2 ⊢ (𝐵 ∈ 𝑉 → (𝐴 × {𝐵}):𝐴⟶{𝐵})
2	1	ffnd 6714	1 ⊢ (𝐵 ∈ 𝑉 → (𝐴 × {𝐵}) Fn 𝐴)

Syntax hints:   → wi 4   ∈ wcel 2107  {csn 4626   × cxp 5672   Fn wfn 6534

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5297  ax-nul 5304  ax-pr 5425

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-nul 4321  df-if 4527  df-sn 4627  df-pr 4629  df-op 4633  df-br 5147  df-opab 5209  df-mpt 5230  df-id 5572  df-xp 5680  df-rel 5681  df-cnv 5682  df-co 5683  df-dm 5684  df-rn 5685  df-fun 6541  df-fn 6542  df-f 6543

This theorem is referenced by:  fconst2g  7198  ofc1  7690  ofc2  7691  caofid0l  7695  caofid0r  7696  caofid1  7697  caofid2  7698  fnsuppres  8170  fczsupp0  8172  fczfsuppd  9376  brwdom2  9563  cantnf0  9665  ofnegsub  12205  ofsubge0  12206  pwsplusgval  17431  pwsmulrval  17432  pwsvscafval  17435  pwsco1mhm  18708  dprdsubg  19885  pwsmgp  20129  pwssplit1  20657  frlmpwsfi  21290  frlmbas  21293  frlmvscaval  21306  islindf4  21376  tmdgsum2  23581  0plef  25170  0pledm  25171  itg1ge0  25184  mbfi1fseqlem5  25218  xrge0f  25230  itg2ge0  25234  itg2addlem  25257  bddibl  25338  dvidlem  25413  rolle  25488  dveq0  25498  dv11cn  25499  tdeglem4  25558  tdeglem4OLD  25559  mdeg0  25569  fta1blem  25667  qaa  25817  basellem9  26572  noextendseq  27149  noetainflem4  27222  fdifsuppconst  31888  elrspunidl  32503  ofcc  33041  ofcof  33042  eulerpartlemt  33307  matunitlindflem1  36421  matunitlindflem2  36422  ptrecube  36425  poimirlem1  36426  poimirlem2  36427  poimirlem3  36428  poimirlem4  36429  poimirlem5  36430  poimirlem6  36431  poimirlem7  36432  poimirlem10  36435  poimirlem11  36436  poimirlem12  36437  poimirlem16  36441  poimirlem17  36442  poimirlem19  36444  poimirlem20  36445  poimirlem22  36447  poimirlem23  36448  poimirlem28  36453  poimirlem29  36454  poimirlem31  36456  poimirlem32  36457  broucube  36459  cnpwstotbnd  36602  eqlkr2  37907  fsuppssind  41114  pwssplit4  41763  mpaaeu  41824  rngunsnply  41847  ofoaid1  42040  ofoaid2  42041  naddcnffo  42046  ofdivrec  43017  dvconstbi  43025  zlmodzxzscm  46934  aacllem  47749