Theorem fnconstg 6768

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

Syntax hints:   → wi 4   ∈ wcel 2143  {csn 4590   × cxp 5661   Fn wfn 6533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-pr 5406

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-fun 6540  df-fn 6541  df-f 6542

This theorem is referenced by:  fconst2g  7203  ofc1  7704  ofc2  7705  caofid0l  7709  caofid0r  7710  caofid1  7711  caofid2  7712  fnsuppres  8188  fczsupp0  8190  fczfsuppd  9347  brwdom2  9536  cantnf0  9645  ofnegsub  12217  ofsubge0  12218  pwsplusgval  17545  pwsmulrval  17546  pwsvscafval  17549  pwsco1mhm  18892  dprdsubg  20097  pwsmgp  20409  pwssplit1  21161  frlmpwsfi  21883  frlmbas  21886  frlmvscaval  21899  islindf4  21969  psrascl  22109  tmdgsum2  24234  0plef  25812  0pledm  25813  itg1ge0  25826  mbfi1fseqlem5  25859  xrge0f  25871  itg2ge0  25875  itg2addlem  25898  bddibl  25980  dvidlem  26055  rolle  26130  dveq0  26140  dv11cn  26141  tdeglem4  26198  mdeg0  26208  fta1blem  26309  qaa  26465  basellem9  27231  noextendseq  27809  noetainflem4  27882  constcof  32944  fdifsuppconst  33012  elrspunidl  33714  ofcc  34474  ofcof  34475  eulerpartlemt  34739  matunitlindflem1  38245  matunitlindflem2  38246  ptrecube  38249  poimirlem1  38250  poimirlem2  38251  poimirlem3  38252  poimirlem4  38253  poimirlem5  38254  poimirlem6  38255  poimirlem7  38256  poimirlem10  38259  poimirlem11  38260  poimirlem12  38261  poimirlem16  38265  poimirlem17  38266  poimirlem19  38268  poimirlem20  38269  poimirlem22  38271  poimirlem23  38272  poimirlem28  38277  poimirlem29  38278  poimirlem31  38280  poimirlem32  38281  broucube  38283  cnpwstotbnd  38426  eqlkr2  39852  fsuppssind  43305  pwssplit4  43796  mpaaeu  43857  rngunsnply  43876  ofoaid1  44065  ofoaid2  44066  naddcnffo  44071  ofdivrec  45016  dvconstbi  45024  zlmodzxzscm  49114  nelsubclem  49822  aacllem  50578