Theorem fnconstg 6751

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

Syntax hints:   → wi 4   ∈ wcel 2109  {csn 4592   × cxp 5639   Fn wfn 6509

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-fun 6516  df-fn 6517  df-f 6518

This theorem is referenced by:  fconst2g  7180  ofc1  7684  ofc2  7685  caofid0l  7689  caofid0r  7690  caofid1  7691  caofid2  7692  fnsuppres  8173  fczsupp0  8175  fczfsuppd  9344  brwdom2  9533  cantnf0  9635  ofnegsub  12191  ofsubge0  12192  pwsplusgval  17460  pwsmulrval  17461  pwsvscafval  17464  pwsco1mhm  18766  dprdsubg  19963  pwsmgp  20243  pwssplit1  20973  frlmpwsfi  21668  frlmbas  21671  frlmvscaval  21684  islindf4  21754  psrascl  21895  tmdgsum2  23990  0plef  25580  0pledm  25581  itg1ge0  25594  mbfi1fseqlem5  25627  xrge0f  25639  itg2ge0  25643  itg2addlem  25666  bddibl  25748  dvidlem  25823  rolle  25901  dveq0  25912  dv11cn  25913  tdeglem4  25972  mdeg0  25982  fta1blem  26083  qaa  26238  basellem9  27006  noextendseq  27586  noetainflem4  27659  fdifsuppconst  32619  elrspunidl  33406  ofcc  34103  ofcof  34104  eulerpartlemt  34369  matunitlindflem1  37617  matunitlindflem2  37618  ptrecube  37621  poimirlem1  37622  poimirlem2  37623  poimirlem3  37624  poimirlem4  37625  poimirlem5  37626  poimirlem6  37627  poimirlem7  37628  poimirlem10  37631  poimirlem11  37632  poimirlem12  37633  poimirlem16  37637  poimirlem17  37638  poimirlem19  37640  poimirlem20  37641  poimirlem22  37643  poimirlem23  37644  poimirlem28  37649  poimirlem29  37650  poimirlem31  37652  poimirlem32  37653  broucube  37655  cnpwstotbnd  37798  eqlkr2  39100  fsuppssind  42588  pwssplit4  43085  mpaaeu  43146  rngunsnply  43165  ofoaid1  43354  ofoaid2  43355  naddcnffo  43360  ofdivrec  44322  dvconstbi  44330  zlmodzxzscm  48349  nelsubclem  49060  aacllem  49794