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 2114  {csn 4568   × 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 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 5231  ax-pr 5370

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 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-mpt 5168  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  7151  ofc1  7652  ofc2  7653  caofid0l  7657  caofid0r  7658  caofid1  7659  caofid2  7660  fnsuppres  8134  fczsupp0  8136  fczfsuppd  9292  brwdom2  9481  cantnf0  9587  ofnegsub  12148  ofsubge0  12149  pwsplusgval  17445  pwsmulrval  17446  pwsvscafval  17449  pwsco1mhm  18791  dprdsubg  19992  pwsmgp  20297  pwssplit1  21046  frlmpwsfi  21742  frlmbas  21745  frlmvscaval  21758  islindf4  21828  psrascl  21967  tmdgsum2  24071  0plef  25649  0pledm  25650  itg1ge0  25663  mbfi1fseqlem5  25696  xrge0f  25708  itg2ge0  25712  itg2addlem  25735  bddibl  25817  dvidlem  25892  rolle  25967  dveq0  25977  dv11cn  25978  tdeglem4  26035  mdeg0  26045  fta1blem  26146  qaa  26300  basellem9  27066  noextendseq  27645  noetainflem4  27718  constcof  32709  fdifsuppconst  32777  elrspunidl  33503  ofcc  34266  ofcof  34267  eulerpartlemt  34531  matunitlindflem1  37951  matunitlindflem2  37952  ptrecube  37955  poimirlem1  37956  poimirlem2  37957  poimirlem3  37958  poimirlem4  37959  poimirlem5  37960  poimirlem6  37961  poimirlem7  37962  poimirlem10  37965  poimirlem11  37966  poimirlem12  37967  poimirlem16  37971  poimirlem17  37972  poimirlem19  37974  poimirlem20  37975  poimirlem22  37977  poimirlem23  37978  poimirlem28  37983  poimirlem29  37984  poimirlem31  37986  poimirlem32  37987  broucube  37989  cnpwstotbnd  38132  eqlkr2  39560  fsuppssind  43040  pwssplit4  43535  mpaaeu  43596  rngunsnply  43615  ofoaid1  43804  ofoaid2  43805  naddcnffo  43810  ofdivrec  44771  dvconstbi  44779  zlmodzxzscm  48845  nelsubclem  49554  aacllem  50288