Theorem fnconstg 6671

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

Syntax hints:   → wi 4   ∈ wcel 2107  {csn 4562   × cxp 5588   Fn wfn 6432

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-sep 5224  ax-nul 5231  ax-pr 5353

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-br 5076  df-opab 5138  df-mpt 5159  df-id 5490  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-fun 6439  df-fn 6440  df-f 6441

This theorem is referenced by:  fconst2g  7087  ofc1  7568  ofc2  7569  caofid0l  7573  caofid0r  7574  caofid1  7575  caofid2  7576  fnsuppres  8016  fczsupp0  8018  fczfsuppd  9155  brwdom2  9341  cantnf0  9442  ofnegsub  11980  ofsubge0  11981  pwsplusgval  17210  pwsmulrval  17211  pwsvscafval  17214  pwsco1mhm  18479  dprdsubg  19636  pwsmgp  19866  pwssplit1  20330  frlmpwsfi  20968  frlmbas  20971  frlmvscaval  20984  islindf4  21054  tmdgsum2  23256  0plef  24845  0pledm  24846  itg1ge0  24859  mbfi1fseqlem5  24893  xrge0f  24905  itg2ge0  24909  itg2addlem  24932  bddibl  25013  dvidlem  25088  rolle  25163  dveq0  25173  dv11cn  25174  tdeglem4  25233  tdeglem4OLD  25234  mdeg0  25244  fta1blem  25342  qaa  25492  basellem9  26247  fdifsuppconst  31032  elrspunidl  31615  ofcc  32083  ofcof  32084  eulerpartlemt  32347  noextendseq  33879  noetainflem4  33952  matunitlindflem1  35782  matunitlindflem2  35783  ptrecube  35786  poimirlem1  35787  poimirlem2  35788  poimirlem3  35789  poimirlem4  35790  poimirlem5  35791  poimirlem6  35792  poimirlem7  35793  poimirlem10  35796  poimirlem11  35797  poimirlem12  35798  poimirlem16  35802  poimirlem17  35803  poimirlem19  35805  poimirlem20  35806  poimirlem22  35808  poimirlem23  35809  poimirlem28  35814  poimirlem29  35815  poimirlem31  35817  poimirlem32  35818  broucube  35820  cnpwstotbnd  35964  eqlkr2  37121  fsuppssind  40289  mhphf  40292  pwssplit4  40921  mpaaeu  40982  rngunsnply  41005  ofdivrec  41951  dvconstbi  41959  zlmodzxzscm  45704  aacllem  46516