Theorem fnconstg 6711

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

Syntax hints:   → wi 4   ∈ wcel 2111  {csn 4576   × cxp 5614   Fn wfn 6476

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 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pr 5370

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 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-br 5092  df-opab 5154  df-mpt 5173  df-id 5511  df-xp 5622  df-rel 5623  df-cnv 5624  df-co 5625  df-dm 5626  df-rn 5627  df-fun 6483  df-fn 6484  df-f 6485

This theorem is referenced by:  fconst2g  7137  ofc1  7638  ofc2  7639  caofid0l  7643  caofid0r  7644  caofid1  7645  caofid2  7646  fnsuppres  8121  fczsupp0  8123  fczfsuppd  9270  brwdom2  9459  cantnf0  9565  ofnegsub  12120  ofsubge0  12121  pwsplusgval  17391  pwsmulrval  17392  pwsvscafval  17395  pwsco1mhm  18737  dprdsubg  19936  pwsmgp  20243  pwssplit1  20991  frlmpwsfi  21687  frlmbas  21690  frlmvscaval  21703  islindf4  21773  psrascl  21914  tmdgsum2  24009  0plef  25598  0pledm  25599  itg1ge0  25612  mbfi1fseqlem5  25645  xrge0f  25657  itg2ge0  25661  itg2addlem  25684  bddibl  25766  dvidlem  25841  rolle  25919  dveq0  25930  dv11cn  25931  tdeglem4  25990  mdeg0  26000  fta1blem  26101  qaa  26256  basellem9  27024  noextendseq  27604  noetainflem4  27677  constcof  32599  fdifsuppconst  32665  elrspunidl  33388  ofcc  34114  ofcof  34115  eulerpartlemt  34379  matunitlindflem1  37655  matunitlindflem2  37656  ptrecube  37659  poimirlem1  37660  poimirlem2  37661  poimirlem3  37662  poimirlem4  37663  poimirlem5  37664  poimirlem6  37665  poimirlem7  37666  poimirlem10  37669  poimirlem11  37670  poimirlem12  37671  poimirlem16  37675  poimirlem17  37676  poimirlem19  37678  poimirlem20  37679  poimirlem22  37681  poimirlem23  37682  poimirlem28  37687  poimirlem29  37688  poimirlem31  37690  poimirlem32  37691  broucube  37693  cnpwstotbnd  37836  eqlkr2  39138  fsuppssind  42625  pwssplit4  43121  mpaaeu  43182  rngunsnply  43201  ofoaid1  43390  ofoaid2  43391  naddcnffo  43396  ofdivrec  44358  dvconstbi  44366  zlmodzxzscm  48387  nelsubclem  49098  aacllem  49832