Theorem fnconstg 6756

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

Syntax hints:   → wi 4   ∈ wcel 2145  {csn 4585   × cxp 5650   Fn wfn 6520

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5251  ax-pr 5395

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-br 5106  df-opab 5168  df-mpt 5187  df-id 5547  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-fun 6527  df-fn 6528  df-f 6529

This theorem is referenced by:  fconst2g  7191  ofc1  7692  ofc2  7693  caofid0l  7697  caofid0r  7698  caofid1  7699  caofid2  7700  fnsuppres  8175  fczsupp0  8177  fczfsuppd  9334  brwdom2  9523  cantnf0  9632  ofnegsub  12207  ofsubge0  12208  pwsplusgval  17534  pwsmulrval  17535  pwsvscafval  17538  pwsco1mhm  18881  dprdsubg  20087  pwsmgp  20399  pwssplit1  21149  frlmpwsfi  21862  frlmbas  21865  frlmvscaval  21878  islindf4  21948  psrascl  22088  tmdgsum2  24214  0plef  25792  0pledm  25793  itg1ge0  25806  mbfi1fseqlem5  25839  xrge0f  25851  itg2ge0  25855  itg2addlem  25878  bddibl  25960  dvidlem  26035  rolle  26110  dveq0  26120  dv11cn  26121  tdeglem4  26178  mdeg0  26188  fta1blem  26289  qaa  26445  basellem9  27211  noextendseq  27789  noetainflem4  27862  constcof  32878  fdifsuppconst  32946  elrspunidl  33652  ofcc  34413  ofcof  34414  eulerpartlemt  34678  matunitlindflem1  38127  matunitlindflem2  38128  ptrecube  38131  poimirlem1  38132  poimirlem2  38133  poimirlem3  38134  poimirlem4  38135  poimirlem5  38136  poimirlem6  38137  poimirlem7  38138  poimirlem10  38141  poimirlem11  38142  poimirlem12  38143  poimirlem16  38147  poimirlem17  38148  poimirlem19  38150  poimirlem20  38151  poimirlem22  38153  poimirlem23  38154  poimirlem28  38159  poimirlem29  38160  poimirlem31  38162  poimirlem32  38163  broucube  38165  cnpwstotbnd  38308  eqlkr2  39736  fsuppssind  43187  pwssplit4  43678  mpaaeu  43739  rngunsnply  43758  ofoaid1  43947  ofoaid2  43948  naddcnffo  43953  ofdivrec  44900  dvconstbi  44908  zlmodzxzscm  48988  nelsubclem  49696  aacllem  50430