Theorem fnconstg 6716

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

Syntax hints:   → wi 4   ∈ wcel 2113  {csn 4575   × cxp 5617   Fn wfn 6481

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 2182  ax-ext 2705  ax-sep 5236  ax-nul 5246  ax-pr 5372

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 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-br 5094  df-opab 5156  df-mpt 5175  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-fun 6488  df-fn 6489  df-f 6490

This theorem is referenced by:  fconst2g  7143  ofc1  7644  ofc2  7645  caofid0l  7649  caofid0r  7650  caofid1  7651  caofid2  7652  fnsuppres  8127  fczsupp0  8129  fczfsuppd  9277  brwdom2  9466  cantnf0  9572  ofnegsub  12130  ofsubge0  12131  pwsplusgval  17396  pwsmulrval  17397  pwsvscafval  17400  pwsco1mhm  18742  dprdsubg  19940  pwsmgp  20247  pwssplit1  20995  frlmpwsfi  21691  frlmbas  21694  frlmvscaval  21707  islindf4  21777  psrascl  21917  tmdgsum2  24012  0plef  25601  0pledm  25602  itg1ge0  25615  mbfi1fseqlem5  25648  xrge0f  25660  itg2ge0  25664  itg2addlem  25687  bddibl  25769  dvidlem  25844  rolle  25922  dveq0  25933  dv11cn  25934  tdeglem4  25993  mdeg0  26003  fta1blem  26104  qaa  26259  basellem9  27027  noextendseq  27607  noetainflem4  27680  constcof  32606  fdifsuppconst  32674  elrspunidl  33400  ofcc  34140  ofcof  34141  eulerpartlemt  34405  matunitlindflem1  37676  matunitlindflem2  37677  ptrecube  37680  poimirlem1  37681  poimirlem2  37682  poimirlem3  37683  poimirlem4  37684  poimirlem5  37685  poimirlem6  37686  poimirlem7  37687  poimirlem10  37690  poimirlem11  37691  poimirlem12  37692  poimirlem16  37696  poimirlem17  37697  poimirlem19  37699  poimirlem20  37700  poimirlem22  37702  poimirlem23  37703  poimirlem28  37708  poimirlem29  37709  poimirlem31  37711  poimirlem32  37712  broucube  37714  cnpwstotbnd  37857  eqlkr2  39219  fsuppssind  42711  pwssplit4  43206  mpaaeu  43267  rngunsnply  43286  ofoaid1  43475  ofoaid2  43476  naddcnffo  43481  ofdivrec  44443  dvconstbi  44451  zlmodzxzscm  48481  nelsubclem  49192  aacllem  49926