Theorem fnconstg 6331

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

Syntax hints:   → wi 4   ∈ wcel 2166  {csn 4398   × cxp 5341   Fn wfn 6119

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2804  ax-sep 5006  ax-nul 5014  ax-pr 5128

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-mo 2606  df-eu 2641  df-clab 2813  df-cleq 2819  df-clel 2822  df-nfc 2959  df-ne 3001  df-ral 3123  df-rab 3127  df-v 3417  df-dif 3802  df-un 3804  df-in 3806  df-ss 3813  df-nul 4146  df-if 4308  df-sn 4399  df-pr 4401  df-op 4405  df-br 4875  df-opab 4937  df-mpt 4954  df-id 5251  df-xp 5349  df-rel 5350  df-cnv 5351  df-co 5352  df-dm 5353  df-rn 5354  df-fun 6126  df-fn 6127  df-f 6128

This theorem is referenced by:  fconst2g  6725  ofc1  7181  ofc2  7182  caofid0l  7186  caofid0r  7187  caofid1  7188  caofid2  7189  fnsuppres  7588  fczsupp0  7590  fczfsuppd  8563  brwdom2  8748  cantnf0  8850  ofnegsub  11349  ofsubge0  11350  pwsplusgval  16504  pwsmulrval  16505  pwsvscafval  16508  xpsc0  16574  xpsc1  16575  pwsco1mhm  17724  dprdsubg  18778  pwsmgp  18973  pwssplit1  19419  frlmpwsfi  20460  frlmbas  20463  frlmvscaval  20475  islindf4  20545  tmdgsum2  22271  0plef  23839  0pledm  23840  itg1ge0  23853  mbfi1fseqlem5  23886  xrge0f  23898  itg2ge0  23902  itg2addlem  23925  bddibl  24006  dvidlem  24079  rolle  24153  dveq0  24163  dv11cn  24164  tdeglem4  24220  mdeg0  24230  fta1blem  24328  qaa  24478  basellem9  25229  ofcc  30714  ofcof  30715  eulerpartlemt  30979  noextendseq  32360  matunitlindflem1  33950  matunitlindflem2  33951  ptrecube  33954  poimirlem1  33955  poimirlem2  33956  poimirlem3  33957  poimirlem4  33958  poimirlem5  33959  poimirlem6  33960  poimirlem7  33961  poimirlem10  33964  poimirlem11  33965  poimirlem12  33966  poimirlem16  33970  poimirlem17  33971  poimirlem19  33973  poimirlem20  33974  poimirlem22  33976  poimirlem23  33977  poimirlem28  33982  poimirlem29  33983  poimirlem31  33985  poimirlem32  33986  broucube  33988  cnpwstotbnd  34139  eqlkr2  35176  pwssplit4  38503  mpaaeu  38564  rngunsnply  38587  ofdivrec  39366  dvconstbi  39374  zlmodzxzscm  42983  aacllem  43444