Theorem fnconstg 6748

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

Syntax hints:   → wi 4   ∈ wcel 2109  {csn 4589   × cxp 5636   Fn wfn 6506

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 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

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 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-fun 6513  df-fn 6514  df-f 6515

This theorem is referenced by:  fconst2g  7177  ofc1  7681  ofc2  7682  caofid0l  7686  caofid0r  7687  caofid1  7688  caofid2  7689  fnsuppres  8170  fczsupp0  8172  fczfsuppd  9337  brwdom2  9526  cantnf0  9628  ofnegsub  12184  ofsubge0  12185  pwsplusgval  17453  pwsmulrval  17454  pwsvscafval  17457  pwsco1mhm  18759  dprdsubg  19956  pwsmgp  20236  pwssplit1  20966  frlmpwsfi  21661  frlmbas  21664  frlmvscaval  21677  islindf4  21747  psrascl  21888  tmdgsum2  23983  0plef  25573  0pledm  25574  itg1ge0  25587  mbfi1fseqlem5  25620  xrge0f  25632  itg2ge0  25636  itg2addlem  25659  bddibl  25741  dvidlem  25816  rolle  25894  dveq0  25905  dv11cn  25906  tdeglem4  25965  mdeg0  25975  fta1blem  26076  qaa  26231  basellem9  26999  noextendseq  27579  noetainflem4  27652  fdifsuppconst  32612  elrspunidl  33399  ofcc  34096  ofcof  34097  eulerpartlemt  34362  matunitlindflem1  37610  matunitlindflem2  37611  ptrecube  37614  poimirlem1  37615  poimirlem2  37616  poimirlem3  37617  poimirlem4  37618  poimirlem5  37619  poimirlem6  37620  poimirlem7  37621  poimirlem10  37624  poimirlem11  37625  poimirlem12  37626  poimirlem16  37630  poimirlem17  37631  poimirlem19  37633  poimirlem20  37634  poimirlem22  37636  poimirlem23  37637  poimirlem28  37642  poimirlem29  37643  poimirlem31  37645  poimirlem32  37646  broucube  37648  cnpwstotbnd  37791  eqlkr2  39093  fsuppssind  42581  pwssplit4  43078  mpaaeu  43139  rngunsnply  43158  ofoaid1  43347  ofoaid2  43348  naddcnffo  43353  ofdivrec  44315  dvconstbi  44323  zlmodzxzscm  48345  nelsubclem  49056  aacllem  49790