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 2108  {csn 4626   × cxp 5683   Fn wfn 6556

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-fun 6563  df-fn 6564  df-f 6565

This theorem is referenced by:  fconst2g  7223  ofc1  7725  ofc2  7726  caofid0l  7730  caofid0r  7731  caofid1  7732  caofid2  7733  fnsuppres  8216  fczsupp0  8218  fczfsuppd  9426  brwdom2  9613  cantnf0  9715  ofnegsub  12264  ofsubge0  12265  pwsplusgval  17535  pwsmulrval  17536  pwsvscafval  17539  pwsco1mhm  18845  dprdsubg  20044  pwsmgp  20324  pwssplit1  21058  frlmpwsfi  21772  frlmbas  21775  frlmvscaval  21788  islindf4  21858  psrascl  21999  tmdgsum2  24104  0plef  25707  0pledm  25708  itg1ge0  25721  mbfi1fseqlem5  25754  xrge0f  25766  itg2ge0  25770  itg2addlem  25793  bddibl  25875  dvidlem  25950  rolle  26028  dveq0  26039  dv11cn  26040  tdeglem4  26099  mdeg0  26109  fta1blem  26210  qaa  26365  basellem9  27132  noextendseq  27712  noetainflem4  27785  fdifsuppconst  32698  elrspunidl  33456  ofcc  34107  ofcof  34108  eulerpartlemt  34373  matunitlindflem1  37623  matunitlindflem2  37624  ptrecube  37627  poimirlem1  37628  poimirlem2  37629  poimirlem3  37630  poimirlem4  37631  poimirlem5  37632  poimirlem6  37633  poimirlem7  37634  poimirlem10  37637  poimirlem11  37638  poimirlem12  37639  poimirlem16  37643  poimirlem17  37644  poimirlem19  37646  poimirlem20  37647  poimirlem22  37649  poimirlem23  37650  poimirlem28  37655  poimirlem29  37656  poimirlem31  37658  poimirlem32  37659  broucube  37661  cnpwstotbnd  37804  eqlkr2  39101  fsuppssind  42603  pwssplit4  43101  mpaaeu  43162  rngunsnply  43181  ofoaid1  43371  ofoaid2  43372  naddcnffo  43377  ofdivrec  44345  dvconstbi  44353  zlmodzxzscm  48273  aacllem  49320