Theorem fnconstg 6541

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

Syntax hints:   → wi 4   ∈ wcel 2111  {csn 4525   × cxp 5517   Fn wfn 6319

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pr 5295

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-v 3443  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-fun 6326  df-fn 6327  df-f 6328

This theorem is referenced by:  fconst2g  6942  ofc1  7412  ofc2  7413  caofid0l  7417  caofid0r  7418  caofid1  7419  caofid2  7420  fnsuppres  7840  fczsupp0  7842  fczfsuppd  8835  brwdom2  9021  cantnf0  9122  ofnegsub  11623  ofsubge0  11624  pwsplusgval  16755  pwsmulrval  16756  pwsvscafval  16759  pwsco1mhm  17988  dprdsubg  19139  pwsmgp  19364  pwssplit1  19824  frlmpwsfi  20441  frlmbas  20444  frlmvscaval  20457  islindf4  20527  tmdgsum2  22701  0plef  24276  0pledm  24277  itg1ge0  24290  mbfi1fseqlem5  24323  xrge0f  24335  itg2ge0  24339  itg2addlem  24362  bddibl  24443  dvidlem  24518  rolle  24593  dveq0  24603  dv11cn  24604  tdeglem4  24661  mdeg0  24671  fta1blem  24769  qaa  24919  basellem9  25674  fdifsuppconst  30449  elrspunidl  31014  ofcc  31475  ofcof  31476  eulerpartlemt  31739  noextendseq  33287  matunitlindflem1  35053  matunitlindflem2  35054  ptrecube  35057  poimirlem1  35058  poimirlem2  35059  poimirlem3  35060  poimirlem4  35061  poimirlem5  35062  poimirlem6  35063  poimirlem7  35064  poimirlem10  35067  poimirlem11  35068  poimirlem12  35069  poimirlem16  35073  poimirlem17  35074  poimirlem19  35076  poimirlem20  35077  poimirlem22  35079  poimirlem23  35080  poimirlem28  35085  poimirlem29  35086  poimirlem31  35088  poimirlem32  35089  broucube  35091  cnpwstotbnd  35235  eqlkr2  36396  fsuppssind  39459  pwssplit4  40033  mpaaeu  40094  rngunsnply  40117  ofdivrec  41030  dvconstbi  41038  zlmodzxzscm  44759  aacllem  45329