Theorem fnconstg 6722

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

Syntax hints:   → wi 4   ∈ wcel 2113  {csn 4580   × cxp 5622   Fn wfn 6487

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-fun 6494  df-fn 6495  df-f 6496

This theorem is referenced by:  fconst2g  7149  ofc1  7650  ofc2  7651  caofid0l  7655  caofid0r  7656  caofid1  7657  caofid2  7658  fnsuppres  8133  fczsupp0  8135  fczfsuppd  9289  brwdom2  9478  cantnf0  9584  ofnegsub  12143  ofsubge0  12144  pwsplusgval  17411  pwsmulrval  17412  pwsvscafval  17415  pwsco1mhm  18757  dprdsubg  19955  pwsmgp  20262  pwssplit1  21011  frlmpwsfi  21707  frlmbas  21710  frlmvscaval  21723  islindf4  21793  psrascl  21934  tmdgsum2  24040  0plef  25629  0pledm  25630  itg1ge0  25643  mbfi1fseqlem5  25676  xrge0f  25688  itg2ge0  25692  itg2addlem  25715  bddibl  25797  dvidlem  25872  rolle  25950  dveq0  25961  dv11cn  25962  tdeglem4  26021  mdeg0  26031  fta1blem  26132  qaa  26287  basellem9  27055  noextendseq  27635  noetainflem4  27708  constcof  32699  fdifsuppconst  32768  elrspunidl  33509  ofcc  34263  ofcof  34264  eulerpartlemt  34528  matunitlindflem1  37813  matunitlindflem2  37814  ptrecube  37817  poimirlem1  37818  poimirlem2  37819  poimirlem3  37820  poimirlem4  37821  poimirlem5  37822  poimirlem6  37823  poimirlem7  37824  poimirlem10  37827  poimirlem11  37828  poimirlem12  37829  poimirlem16  37833  poimirlem17  37834  poimirlem19  37836  poimirlem20  37837  poimirlem22  37839  poimirlem23  37840  poimirlem28  37845  poimirlem29  37846  poimirlem31  37848  poimirlem32  37849  broucube  37851  cnpwstotbnd  37994  eqlkr2  39356  fsuppssind  42832  pwssplit4  43327  mpaaeu  43388  rngunsnply  43407  ofoaid1  43596  ofoaid2  43597  naddcnffo  43602  ofdivrec  44563  dvconstbi  44571  zlmodzxzscm  48599  nelsubclem  49308  aacllem  50042