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 2119  {csn 4562   × cxp 5623   Fn wfn 6487

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-pr 5369

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-br 5080  df-opab 5142  df-mpt 5161  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-fun 6494  df-fn 6495  df-f 6496

This theorem is referenced by:  fconst2g  7154  ofc1  7655  ofc2  7656  caofid0l  7660  caofid0r  7661  caofid1  7662  caofid2  7663  fnsuppres  8138  fczsupp0  8140  fczfsuppd  9296  brwdom2  9485  cantnf0  9594  ofnegsub  12155  ofsubge0  12156  pwsplusgval  17452  pwsmulrval  17453  pwsvscafval  17456  pwsco1mhm  18798  dprdsubg  19999  pwsmgp  20304  pwssplit1  21056  frlmpwsfi  21734  frlmbas  21737  frlmvscaval  21750  islindf4  21820  psrascl  21960  tmdgsum2  24086  0plef  25664  0pledm  25665  itg1ge0  25678  mbfi1fseqlem5  25711  xrge0f  25723  itg2ge0  25727  itg2addlem  25750  bddibl  25832  dvidlem  25907  rolle  25982  dveq0  25992  dv11cn  25993  tdeglem4  26050  mdeg0  26060  fta1blem  26161  qaa  26314  basellem9  27077  noextendseq  27656  noetainflem4  27729  constcof  32720  fdifsuppconst  32788  elrspunidl  33518  ofcc  34297  ofcof  34298  eulerpartlemt  34562  matunitlindflem1  37990  matunitlindflem2  37991  ptrecube  37994  poimirlem1  37995  poimirlem2  37996  poimirlem3  37997  poimirlem4  37998  poimirlem5  37999  poimirlem6  38000  poimirlem7  38001  poimirlem10  38004  poimirlem11  38005  poimirlem12  38006  poimirlem16  38010  poimirlem17  38011  poimirlem19  38013  poimirlem20  38014  poimirlem22  38016  poimirlem23  38017  poimirlem28  38022  poimirlem29  38023  poimirlem31  38025  poimirlem32  38026  broucube  38028  cnpwstotbnd  38171  eqlkr2  39599  fsuppssind  43050  pwssplit4  43541  mpaaeu  43602  rngunsnply  43621  ofoaid1  43810  ofoaid2  43811  naddcnffo  43816  ofdivrec  44777  dvconstbi  44785  zlmodzxzscm  48855  nelsubclem  49564  aacllem  50298