Theorem fnconstg 6646

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

Syntax hints:   → wi 4   ∈ wcel 2108  {csn 4558   × cxp 5578   Fn wfn 6413

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-fun 6420  df-fn 6421  df-f 6422

This theorem is referenced by:  fconst2g  7060  ofc1  7537  ofc2  7538  caofid0l  7542  caofid0r  7543  caofid1  7544  caofid2  7545  fnsuppres  7978  fczsupp0  7980  fczfsuppd  9076  brwdom2  9262  cantnf0  9363  ofnegsub  11901  ofsubge0  11902  pwsplusgval  17118  pwsmulrval  17119  pwsvscafval  17122  pwsco1mhm  18385  dprdsubg  19542  pwsmgp  19772  pwssplit1  20236  frlmpwsfi  20869  frlmbas  20872  frlmvscaval  20885  islindf4  20955  tmdgsum2  23155  0plef  24741  0pledm  24742  itg1ge0  24755  mbfi1fseqlem5  24789  xrge0f  24801  itg2ge0  24805  itg2addlem  24828  bddibl  24909  dvidlem  24984  rolle  25059  dveq0  25069  dv11cn  25070  tdeglem4  25129  tdeglem4OLD  25130  mdeg0  25140  fta1blem  25238  qaa  25388  basellem9  26143  fdifsuppconst  30925  elrspunidl  31508  ofcc  31974  ofcof  31975  eulerpartlemt  32238  noextendseq  33797  noetainflem4  33870  matunitlindflem1  35700  matunitlindflem2  35701  ptrecube  35704  poimirlem1  35705  poimirlem2  35706  poimirlem3  35707  poimirlem4  35708  poimirlem5  35709  poimirlem6  35710  poimirlem7  35711  poimirlem10  35714  poimirlem11  35715  poimirlem12  35716  poimirlem16  35720  poimirlem17  35721  poimirlem19  35723  poimirlem20  35724  poimirlem22  35726  poimirlem23  35727  poimirlem28  35732  poimirlem29  35733  poimirlem31  35735  poimirlem32  35736  broucube  35738  cnpwstotbnd  35882  eqlkr2  37041  fsuppssind  40205  mhphf  40208  pwssplit4  40830  mpaaeu  40891  rngunsnply  40914  ofdivrec  41833  dvconstbi  41841  zlmodzxzscm  45581  aacllem  46391