Theorem fnconstg 6233

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 6232	. 2 ⊢ (𝐵 ∈ 𝑉 → (𝐴 × {𝐵}):𝐴⟶{𝐵})
2		ffn 6185	. 2 ⊢ ((𝐴 × {𝐵}):𝐴⟶{𝐵} → (𝐴 × {𝐵}) Fn 𝐴)
3	1, 2	syl 17	1 ⊢ (𝐵 ∈ 𝑉 → (𝐴 × {𝐵}) Fn 𝐴)

Syntax hints:   → wi 4   ∈ wcel 2145  {csn 4316   × cxp 5247   Fn wfn 6026  ⟶wf 6027

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pr 5034

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rab 3070  df-v 3353  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-sn 4317  df-pr 4319  df-op 4323  df-br 4787  df-opab 4847  df-mpt 4864  df-id 5157  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-fun 6033  df-fn 6034  df-f 6035

This theorem is referenced by:  fconst2g  6612  ofc1  7067  ofc2  7068  caofid0l  7072  caofid0r  7073  caofid1  7074  caofid2  7075  fnsuppres  7474  fczsupp0  7476  fczfsuppd  8449  brwdom2  8634  cantnf0  8736  ofnegsub  11220  ofsubge0  11221  pwsplusgval  16358  pwsmulrval  16359  pwsvscafval  16362  xpsc0  16428  xpsc1  16429  pwsco1mhm  17578  dprdsubg  18631  pwsmgp  18826  pwssplit1  19272  frlmpwsfi  20313  frlmbas  20316  frlmvscaval  20327  islindf4  20394  tmdgsum2  22120  0plef  23659  0pledm  23660  itg1ge0  23673  mbfi1fseqlem5  23706  xrge0f  23718  itg2ge0  23722  itg2addlem  23745  bddibl  23826  dvidlem  23899  rolle  23973  dveq0  23983  dv11cn  23984  tdeglem4  24040  mdeg0  24050  fta1blem  24148  qaa  24298  basellem9  25036  ofcc  30508  ofcof  30509  eulerpartlemt  30773  noextendseq  32157  matunitlindflem1  33738  matunitlindflem2  33739  ptrecube  33742  poimirlem1  33743  poimirlem2  33744  poimirlem3  33745  poimirlem4  33746  poimirlem5  33747  poimirlem6  33748  poimirlem7  33749  poimirlem10  33752  poimirlem11  33753  poimirlem12  33754  poimirlem16  33758  poimirlem17  33759  poimirlem19  33761  poimirlem20  33762  poimirlem22  33764  poimirlem23  33765  poimirlem28  33770  poimirlem29  33771  poimirlem31  33773  poimirlem32  33774  broucube  33776  cnpwstotbnd  33928  eqlkr2  34909  pwssplit4  38185  mpaaeu  38246  rngunsnply  38269  ofdivrec  39051  dvconstbi  39059  zlmodzxzscm  42663  aacllem  43078