Theorem fnconstg 6766

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

Syntax hints:   → wi 4   ∈ wcel 2108  {csn 4601   × cxp 5652   Fn wfn 6526

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

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 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-fun 6533  df-fn 6534  df-f 6535

This theorem is referenced by:  fconst2g  7195  ofc1  7699  ofc2  7700  caofid0l  7704  caofid0r  7705  caofid1  7706  caofid2  7707  fnsuppres  8190  fczsupp0  8192  fczfsuppd  9398  brwdom2  9587  cantnf0  9689  ofnegsub  12238  ofsubge0  12239  pwsplusgval  17504  pwsmulrval  17505  pwsvscafval  17508  pwsco1mhm  18810  dprdsubg  20007  pwsmgp  20287  pwssplit1  21017  frlmpwsfi  21712  frlmbas  21715  frlmvscaval  21728  islindf4  21798  psrascl  21939  tmdgsum2  24034  0plef  25625  0pledm  25626  itg1ge0  25639  mbfi1fseqlem5  25672  xrge0f  25684  itg2ge0  25688  itg2addlem  25711  bddibl  25793  dvidlem  25868  rolle  25946  dveq0  25957  dv11cn  25958  tdeglem4  26017  mdeg0  26027  fta1blem  26128  qaa  26283  basellem9  27051  noextendseq  27631  noetainflem4  27704  fdifsuppconst  32666  elrspunidl  33443  ofcc  34137  ofcof  34138  eulerpartlemt  34403  matunitlindflem1  37640  matunitlindflem2  37641  ptrecube  37644  poimirlem1  37645  poimirlem2  37646  poimirlem3  37647  poimirlem4  37648  poimirlem5  37649  poimirlem6  37650  poimirlem7  37651  poimirlem10  37654  poimirlem11  37655  poimirlem12  37656  poimirlem16  37660  poimirlem17  37661  poimirlem19  37663  poimirlem20  37664  poimirlem22  37666  poimirlem23  37667  poimirlem28  37672  poimirlem29  37673  poimirlem31  37675  poimirlem32  37676  broucube  37678  cnpwstotbnd  37821  eqlkr2  39118  fsuppssind  42616  pwssplit4  43113  mpaaeu  43174  rngunsnply  43193  ofoaid1  43382  ofoaid2  43383  naddcnffo  43388  ofdivrec  44350  dvconstbi  44358  zlmodzxzscm  48332  nelsubclem  49034  aacllem  49665