Theorem fnconstg 6730

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

Syntax hints:   → wi 4   ∈ wcel 2114  {csn 4582   × cxp 5630   Fn wfn 6495

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-fun 6502  df-fn 6503  df-f 6504

This theorem is referenced by:  fconst2g  7159  ofc1  7660  ofc2  7661  caofid0l  7665  caofid0r  7666  caofid1  7667  caofid2  7668  fnsuppres  8143  fczsupp0  8145  fczfsuppd  9301  brwdom2  9490  cantnf0  9596  ofnegsub  12155  ofsubge0  12156  pwsplusgval  17423  pwsmulrval  17424  pwsvscafval  17427  pwsco1mhm  18769  dprdsubg  19967  pwsmgp  20274  pwssplit1  21023  frlmpwsfi  21719  frlmbas  21722  frlmvscaval  21735  islindf4  21805  psrascl  21946  tmdgsum2  24052  0plef  25641  0pledm  25642  itg1ge0  25655  mbfi1fseqlem5  25688  xrge0f  25700  itg2ge0  25704  itg2addlem  25727  bddibl  25809  dvidlem  25884  rolle  25962  dveq0  25973  dv11cn  25974  tdeglem4  26033  mdeg0  26043  fta1blem  26144  qaa  26299  basellem9  27067  noextendseq  27647  noetainflem4  27720  constcof  32710  fdifsuppconst  32778  elrspunidl  33520  ofcc  34283  ofcof  34284  eulerpartlemt  34548  matunitlindflem1  37861  matunitlindflem2  37862  ptrecube  37865  poimirlem1  37866  poimirlem2  37867  poimirlem3  37868  poimirlem4  37869  poimirlem5  37870  poimirlem6  37871  poimirlem7  37872  poimirlem10  37875  poimirlem11  37876  poimirlem12  37877  poimirlem16  37881  poimirlem17  37882  poimirlem19  37884  poimirlem20  37885  poimirlem22  37887  poimirlem23  37888  poimirlem28  37893  poimirlem29  37894  poimirlem31  37896  poimirlem32  37897  broucube  37899  cnpwstotbnd  38042  eqlkr2  39470  fsuppssind  42945  pwssplit4  43440  mpaaeu  43501  rngunsnply  43520  ofoaid1  43709  ofoaid2  43710  naddcnffo  43715  ofdivrec  44676  dvconstbi  44684  zlmodzxzscm  48711  nelsubclem  49420  aacllem  50154